toNonUnitalStarSubalgebra_toStarSubalgebra

English

Let S be a star-subalgebra of A over R. If we view S as a nonunital star-subalgebra and then reconstruct a star-subalgebra from the unit membership S.one_mem', we obtain the original S.

Русский

Пусть S — звездо-подалгебра кольца A над R. Если рассмотреть S как нестандартную звездо-подалгебру без единицы и затем воссоздать звездо-подалгебру, используя свойство существования единицы в S (1 ∈ S), то получаем исходную S.

LaTeX

$$$ S.toNonUnitalStarSubalgebra.toStarSubalgebra\; S.one_mem' = S $$$

Lean4

theorem toNonUnitalStarSubalgebra_toStarSubalgebra (S : StarSubalgebra R A) :
    S.toNonUnitalStarSubalgebra.toStarSubalgebra S.one_mem' = S := by cases S; rfl

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