starClosure_toNonUnitalSubalgebra

English

The coercion from starClosure to its underlying NonUnitalSubalgebra is the identity, i.e., the starClosure maps to the same underlying subalgebra as S ⊔ star S.

Русский

Прямая подстановка из starClosure в его базовый NonUnitalSubalgebra является тождественной: starClosure отображается на ту же базовую подполную, что и S ⊔ star S.

LaTeX

$$$ \text{coe}(S^{*}) = S \cup\!\cup \ star(S) $$$

Lean4

@[simp]
theorem starClosure_toNonUnitalSubalgebra (S : NonUnitalSubalgebra R A) :
    S.starClosure.toNonUnitalSubalgebra = S ⊔ star S :=
  rfl

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