case inl
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ M.toAddSubmonoid ^ 0 ≤ (M ^ 0).toAddSubmonoid

case inr
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
n : ℕ
hn : n ≠ 0
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
n : ℕ
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
obtain rfl | hn := Decidable.eq_or_ne n 0
case inl
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ 1 ≤ 1.toAddSubmonoid
case inl
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ M.toAddSubmonoid ^ 0 ≤ (M ^ 0).toAddSubmonoid
rw [pow_zero, pow_zero]
no goals
case inl
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ 1 ≤ 1.toAddSubmonoid
exact le_one_toAddSubmonoid
no goals
case inr
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
n : ℕ
hn : n ≠ 0
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
exact (pow_toAddSubmonoid M hn).ge