span_eq_toSubmodule — Mathlib

English

For a nonunital subalgebra s of A over R, the span of its carrier as a submodule equals its underlying submodule: Submodule.span R (s : Set A) = s.toSubmodule.

Русский

Для неполной подполинной подалгебры s над A верно: подмодуль, порождённый множеством носителей s, совпадает с её подмодулем-образом.

LaTeX

$$$\operatorname{span}_R\bigl(s\bigr) = s.{\text{toSubmodule}}$$$

Lean4

@[simp]
theorem span_eq_toSubmodule (s : NonUnitalSubalgebra R A) : Submodule.span R (s : Set A) = s.toSubmodule := by
  simp [SetLike.ext'_iff, Submodule.coe_span_eq_self]

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