adjoin_eq_span_of_subset — Mathlib

English

Let R be a commutative semiring and A an R-algebra. For a subset s of A, if the multiplicative closure of s lies inside the R-span of s, then the underlying R-submodule of the subalgebra generated by s equals the R-span of s.

Русский

Пусть R — коммутативное полукольцо, A — R-алгебра. Для подмножества s ⊆ A, если умножительная замкнутость s содержится в линейной оболочке над R от s, то базовый подмодуль подалгебры, порождаемой s, равен span_R(s).

LaTeX

$$$\\operatorname{toSubmodule}(\\operatorname{adjoin}_R s) = \\operatorname{span}_R s$$$

Lean4

theorem adjoin_eq_span_of_subset {s : Set A} (hs : ↑(Submonoid.closure s) ⊆ (span R s : Set A)) :
    Subalgebra.toSubmodule (adjoin R s) = span R s :=
  le_antisymm ((adjoin_toSubmodule_le R).mpr hs) (span_le_adjoin R s)

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