span_set_smul — Mathlib

English

Under the same assumptions, the span of the S-action of s on t equals the S-action of s on the span of t: span_R(s • t) = s • span_R t.

Русский

При тех же предпосылках образующая подмодуль от S-действия множества s на t равна действию s на образующую подмодуль t: span_R(s • t) = s • span_R t.

LaTeX

$$$ \operatorname{span}_R(s \cdot t) = s \cdot \operatorname{span}_R(t) $$$

Lean4

theorem span_set_smul [SMulCommClass S R M] (s : Set S) (t : Set M) : span R (s • t) = s • span R t :=
  (set_smul_span s t).symm

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