English
Two NonUnitalRing structures on R are equal if they have the same additive and multiplicative operations.
Русский
Две структуры NonUnitalRing на R равны, если совпадают их операции сложения и умножения.
LaTeX
$$$\\\\forall A,B \\,\\in \\, \\text{NonUnitalRing}(R), \\\\ (+)_A = (+)_B \\\\land (\\cdot)_A = (\\cdot)_B \\\\Rightarrow A = B.$$$
Lean4
@[ext]
theorem ext ⦃inst₁ inst₂ : NonUnitalRing 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 : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing := by
ext : 1 <;>
assumption
-- Split into fields and prove they are equal using the above.
cases inst₁; cases inst₂
congr
