toNonAssocSemiring_injective — Mathlib

English

The forgetful map to NonAssocSemiring from NonAssocRing is injective.

Русский

Отображение забывания от NonAssocRing к NonAssocSemiring инъективно.

LaTeX

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

Lean4

theorem toNonAssocSemiring_injective : Function.Injective (@toNonAssocSemiring R) :=
  by
  intro _ _ h
  ext x y
  · exact congrArg (·.toAdd.add x y) h
  · exact congrArg (·.toMul.mul x y) h

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