toNonUnitalNonAssocRing_injective

English

The forgetful map toNonUnitalNonAssocRing forgets nothing and is injective.

Русский

Забывающее отображение к NonUnitalNonAssocRing инъективно.

LaTeX

$$$\\\\forall A,B \\,\\in \\, \\text{NonUnitalNonAssocRing}(R), \\\\ toNonUnitalNonAssocRing(A) = toNonUnitalNonAssocRing(B) \\\\Rightarrow A = B.$$$

Lean4

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

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