English
The product of span S and span T equals the span of all s t with s ∈ S and t ∈ T: span S • span T = span { s t | s ∈ S, t ∈ T }.
Русский
Произведение пространств, порождаемых S и T, равно порождению всех элементов s t с s ∈ S и t ∈ T.
LaTeX
$$$\\operatorname{span} S \\cdot \\operatorname{span} T = \\operatorname{span} \\{ s t \\mid s \\in S, t \\in T \\}$$$
Lean4
theorem span_smul_span : Ideal.span S • span R T = span R (⋃ (s ∈ S) (t ∈ T), {s • t}) :=
by
rw [smul_eq_map₂]
exact (map₂_span_span _ _ _ _).trans <| congr_arg _ <| Set.image2_eq_iUnion _ _ _