adjoin_eq_span — Mathlib

English

The adjoint of a subalgebra has its underlying submodule equal to the linear span of the closure of the generating set; i.e., adjoin equals span of the closure.

Русский

У подалгебры с сопряжением подмодуль-образ равен линейному пространству замкнутого порождателя.

LaTeX

$$$\mathrm{StarAlgebra}.adjoin(R,s)^{\text{toSubmodule}} = \mathrm{span}_R(\mathrm{closure}(s \cup s^{*}))$$$

Lean4

theorem adjoin_eq_span (s : Set A) :
    Subalgebra.toSubmodule (adjoin R s).toSubalgebra = span R (Submonoid.closure (s ∪ star s)) := by
  rw [adjoin_toSubalgebra, Algebra.adjoin_eq_span]

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