toSubring_toNonUnitalSubring — Mathlib

English

Converting a NonUnitalSubring back from a Subring yields the original NonUnitalSubring.

Русский

Преобразование подкольца обратно к неуниверсальному подкольцу возвращает исходное неуниверсальное подкольцо.

LaTeX

$$$ (\text{toSubring}(S,h_1)).\text{toNonUnitalSubring} = S$$$

Lean4

theorem toSubring_toNonUnitalSubring (S : NonUnitalSubring R) (h1 : (1 : R) ∈ S) :
    (NonUnitalSubring.toSubring S h1).toNonUnitalSubring = S := by cases S; rfl

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