no goals
ι : 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
s : Set A
⊢ span R s ^ 0 = span R (s ^ 0)
rw [pow_zero, pow_zero, one_eq_span_one_set]
no goals
ι : 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
s : Set A
n : ℕ
⊢ span R s ^ (n + 1) = span R (s ^ (n + 1))
rw [pow_succ, pow_succ, span_pow s n, span_mul_span]