toSubalgebra_toNonUnitalSubalgebra

English

Similarly, the roundtrip from a NonUnitalSubalgebra to Subalgebra and back yields the original nonunital subalgebra.

Русский

Аналогично, повторная процедура от неунитального подалгебра обратно к неунитальному сохраняет исходную структуру.

LaTeX

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

Lean4

theorem toSubalgebra_toNonUnitalSubalgebra (S : NonUnitalSubalgebra R A) (h1 : (1 : A) ∈ S) :
    (NonUnitalSubalgebra.toSubalgebra S h1).toNonUnitalSubalgebra = S := by cases S; rfl

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