toNonAssocRing_injective — Mathlib

English

Two Ring structures on R are equal if their additive and multiplicative data match in a stepwise fashion.

Русский

Две структуры Ring на R равны, если их данные сложения и умножения совпадают по частям.

LaTeX

$$$\\\\forall A,B \\,\\in \\, \\text{Ring}(R), \\\\ (A{\\\\:}\\\\text{toSemiring}) = (B{\\\\:}\\\\text{toSemiring}) \\\\land (A{\\\\:}\\\\text{toNonAssocRing}) = (B{\\\\:}\\\\text{toNonAssocRing}) \\\\Rightarrow A=B.$$$

Lean4

theorem toNonAssocRing_injective : Function.Injective (@toNonAssocRing R) :=
  by
  intro _ _ _
  ext <;> congr

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