toNonUnitalSemiring_injective — Mathlib

English

The map toNonUnitalSemiring from NonUnitalRing is injective.

Русский

Отображение toNonUnitalSemiring от NonUnitalRing инъективно.

LaTeX

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

Lean4

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

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