R : Type u
ι : Type ?u.223899
inst✝ : CommSemiring R
I J K L : Ideal R
r s : R
⊢ Submodule.span R {r} * Submodule.span R {s} = Submodule.span R {r * s}
R : Type u
ι : Type ?u.223899
inst✝ : CommSemiring R
I J K L : Ideal R
r s : R
⊢ span {r} * span {s} = span {r * s}
unfold span
no goals
R : Type u
ι : Type ?u.223899
inst✝ : CommSemiring R
I J K L : Ideal R
r s : R
⊢ Submodule.span R {r} * Submodule.span R {s} = Submodule.span R {r * s}
rw [Submodule.span_mul_span, Set.singleton_mul_singleton]