no goals
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
h : FG M
n : ℕ
⊢ span R ↑{1} = M ^ Nat.zero
simp [one_eq_span]
no goals
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
h : FG M
n✝ n : ℕ
ih : FG (M ^ n)
⊢ FG (M ^ Nat.succ n)
simpa [pow_succ] using h.mul ih