adjoin_toNonUnitalSubalgebra — Mathlib

English

The underlying nonunital subalgebra of adjoin R s agrees with the nonunital algebra generated by s ∪ s*.

Русский

Основание неединичной подпалгебры adjoin R s совпадает с ненулеподалгеброй, порожденной s ∪ s*.

LaTeX

$$$$ (\\\\operatorname{adjoin}_R(s)).toNonUnitalSubalgebra = \\\\operatorname{NonUnitalAlgebra.adjoin}_R(s \\\\cup star(s)) $$$$

Lean4

theorem adjoin_toNonUnitalSubalgebra (s : Set A) :
    (adjoin R s).toNonUnitalSubalgebra = NonUnitalAlgebra.adjoin R (s ∪ star s) :=
  rfl

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