case zero
ι : 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 : ℕ
h✝ : n ≠ 0
h : Nat.zero ≠ 0
⊢ (M ^ Nat.zero).toAddSubmonoid = M.toAddSubmonoid ^ Nat.zero

case succ
ι : 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✝ : ℕ
h✝ : n✝ ≠ 0
n : ℕ
ih : n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : Nat.succ n ≠ 0
⊢ (M ^ Nat.succ n).toAddSubmonoid = M.toAddSubmonoid ^ Nat.succ n
ι : 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 : ℕ
h : n ≠ 0
⊢ (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
induction' n with n ih
no goals
case zero
ι : 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 : ℕ
h✝ : n ≠ 0
h : Nat.zero ≠ 0
⊢ (M ^ Nat.zero).toAddSubmonoid = M.toAddSubmonoid ^ Nat.zero
exact (h rfl).elim
case succ
ι : 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✝ : ℕ
h✝ : n✝ ≠ 0
n : ℕ
ih : n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : Nat.succ n ≠ 0
⊢ M.toAddSubmonoid * (M ^ n).toAddSubmonoid = M.toAddSubmonoid * M.toAddSubmonoid ^ n
case succ
ι : 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✝ : ℕ
h✝ : n✝ ≠ 0
n : ℕ
ih : n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : Nat.succ n ≠ 0
⊢ (M ^ Nat.succ n).toAddSubmonoid = M.toAddSubmonoid ^ Nat.succ n
rw [pow_succ, pow_succ, mul_toAddSubmonoid]
no goals
case succ
ι : 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✝ : ℕ
h✝ : n✝ ≠ 0
n : ℕ
ih : n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : Nat.succ n ≠ 0
⊢ M.toAddSubmonoid * (M ^ n).toAddSubmonoid = M.toAddSubmonoid * M.toAddSubmonoid ^ n
cases n with
| zero => rw [pow_zero, pow_zero, mul_one, ← mul_toAddSubmonoid, mul_one]
| succ n => rw [ih n.succ_ne_zero]
no goals
case succ.zero
ι : 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 : ℕ
h✝ : n ≠ 0
ih : Nat.zero ≠ 0 → (M ^ Nat.zero).toAddSubmonoid = M.toAddSubmonoid ^ Nat.zero
h : Nat.succ Nat.zero ≠ 0
⊢ M.toAddSubmonoid * (M ^ Nat.zero).toAddSubmonoid = M.toAddSubmonoid * M.toAddSubmonoid ^ Nat.zero
rw [pow_zero, pow_zero, mul_one, ← mul_toAddSubmonoid, mul_one]
no goals
case succ.succ
ι : 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✝ : ℕ
h✝ : n✝ ≠ 0
n : ℕ
ih : Nat.succ n ≠ 0 → (M ^ Nat.succ n).toAddSubmonoid = M.toAddSubmonoid ^ Nat.succ n
h : Nat.succ (Nat.succ n) ≠ 0
⊢ M.toAddSubmonoid * (M ^ Nat.succ n).toAddSubmonoid = M.toAddSubmonoid * M.toAddSubmonoid ^ Nat.succ n
rw [ih n.succ_ne_zero]