adjoin_eq_span — Mathlib

English

The underlying submodule of adjoin is the span of the closure of s ∪ s*.

Русский

Подмодуль-основание adjoin равен порождающему подмодуль(span) замыканию по s ∪ s*.

LaTeX

$$$$ (\\\\operatorname{adjoin}_R(s)).toSubmodule = \\\\operatorname{span}_R(\\\\operatorname{Subsemigroup.closure}(s \\cup star(s))) $$$$

Lean4

theorem adjoin_eq_span (s : Set A) : (adjoin R s).toSubmodule = Submodule.span R (Subsemigroup.closure (s ∪ star s)) :=
  by rw [adjoin_toNonUnitalSubalgebra, NonUnitalAlgebra.adjoin_eq_span]

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