set_smul_span — Mathlib

English

Let S act on a module M over a semiring R, and let s ⊆ S and t ⊆ M be sets. Then the submodule generated by the S-action of s on span_R(t) coincides with the span_R of the S-action of s on t: s • span_R(t) = span_R(s • t).

Русский

Пусть S действует на модуль M над полем/кольцом R; возьмем подмножество s ⊆ S и t ⊆ M. Тогда подмодуль, порожденный действием S на span_R(t), совпадает с span_R(S-действием на t): s • span_R(t) = span_R(s • t).

LaTeX

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

Lean4

theorem set_smul_span [SMulCommClass S R M] (s : Set S) (t : Set M) : s • span R t = span R (s • t) := by
  simp_rw [set_smul_eq_iSup, smul_span, iSup_span, Set.iUnion_smul_set]

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