R : Type u
ι : Type ?u.222969
inst✝ : CommSemiring R
I J K L : Ideal R
S T : Set R
⊢ Submodule.span R S * Submodule.span R T = Submodule.span R (S * T)
R : Type u
ι : Type ?u.222969
inst✝ : CommSemiring R
I J K L : Ideal R
S T : Set R
⊢ span S * span T = span (S * T)
unfold span
no goals
R : Type u
ι : Type ?u.222969
inst✝ : CommSemiring R
I J K L : Ideal R
S T : Set R
⊢ Submodule.span R S * Submodule.span R T = Submodule.span R (S * T)
rw [Submodule.span_mul_span]