toNonUnitalSubalgebra_toSubalgebra

English

The construction S.toNonUnitalSubalgebra followed by S.toSubalgebra returns the original Subalgebra; in short, the unitalization-recovery process is identity on Subalgebras.

Русский

Пусть S — подалгебра; преобразование в неединственную подалгебру затем обратно возвращает исходную подалгебру.

LaTeX

$$$S = (S^{\text{toNonUnitalSubalgebra}})^{\text{toSubalgebra}}$$$

Lean4

theorem toNonUnitalSubalgebra_toSubalgebra (S : Subalgebra R A) : S.toNonUnitalSubalgebra.toSubalgebra S.one_mem = S :=
  by cases S; rfl

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