span_mul_span — Mathlib

English

For sets S and T in a semiring R, span(S) · span(T) = span({ s t | s ∈ S, t ∈ T }).

Русский

Для множеств S и T в полугруппе R справедливо span(S)·span(T) = span({ st | s ∈ S, t ∈ T }).

LaTeX

$$$ \\operatorname{span}(S) \\cdot \\operatorname{span}(T) = \\operatorname{span}(\\{ st : s \\in S, t \\in T \\})$$$

Lean4

theorem span_mul_span (S T : Set R) : span S * span T = span (⋃ (s ∈ S) (t ∈ T), {s * t}) :=
  Submodule.span_smul_span S T

Похожие утверждения