toNonUnitalRing_injective — Mathlib

English

The forgetful map toNonUnitalRing from NonUnitalCommRing is injective; two NonUnitalCommRing structures with the same underlying NonUnitalRing are equal.

Русский

Отображение забывания из NonUnitalCommRing в NonUnitalRing инъективно; две структуры NonUnitalCommRing, имеющие одинаковую подлежащую структуру NonUnitalRing, совпадают.

LaTeX

$$$\\forall R\\, I_1,I_2:\\, \\text{NonUnitalCommRing}(R),\\quad toNonUnitalRing(I_1) = toNonUnitalRing(I_2) \\Rightarrow I_1 = I_2$$$

Lean4

theorem toNonUnitalRing_injective : Function.Injective (@toNonUnitalRing R) := by rintro ⟨⟩ ⟨⟩ _; congr

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