English
Two NonAssocRing structures on R are equal if their additive and multiplicative parts agree.
Русский
Две структуры NonAssocRing на R равны, если их сложение и умножение согласованы.
LaTeX
$$$\\\\forall A,B \\,\\in \\, \\text{NonAssocRing}(R), \\\\ (A{\\\\:}+,A{\\\\:}\\\\cdot)=(B{\\\\:}+,B{\\\\:}\\\\cdot) \\\\Rightarrow A=B.$$$
Lean4
@[ext]
theorem ext ⦃inst₁ inst₂ : NonAssocRing R⦄ (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
(h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : inst₁ = inst₂ :=
by
have h₁ : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing := by ext : 1 <;> assumption
have h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring := by
ext : 1 <;>
assumption
-- Mathematically non-trivial fact: `intCast` is determined by the rest.
have h₃ : inst₁.toAddCommGroupWithOne = inst₂.toAddCommGroupWithOne :=
AddCommGroupWithOne.ext h_add (congrArg (·.toOne.one) h₂)
cases inst₁; cases inst₂
congr <;>
solve
| injection h₁
| injection h₂
| injection h₃
