adjoin_toSubalgebra — Mathlib

English

The underlying subalgebra of the star-subalgebra generated by s is the ordinary subalgebra generated by s ∪ star s: (adjoin R s).toSubalgebra = Algebra.adjoin R (s ∪ star s).

Русский

Механизм подстановки: порождаемые звёздной подалгеброй элементы образуют обычную подалгебру, порождаемую s ∪ star s.

LaTeX

$$$( \\mathrm{adjoin}(R,s) )^{\\;toSubalgebra} = \\mathrm{Algebra.adjoin}(R,\, s \\cup s^{*}).$$$

Lean4

theorem adjoin_toSubalgebra (s : Set A) : (adjoin R s).toSubalgebra = Algebra.adjoin R (s ∪ star s) :=
  rfl

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