English
Two NonUnitalNonAssocRing structures on R are equal if they have the same additive structure and the same multiplicative structure.
Русский
Две структуры NonUnitalNonAssocRing на R равны, если совпадают их аддитивная и мультипликативная структуры.
LaTeX
$$$\\\\forall A,B \\,\\in \\, \\text{NonUnitalNonAssocRing}(R), \\\\ (+)_A = (+)_B \\\\land (\\cdot)_A = (\\cdot)_B \\\\Rightarrow A = B.$$$
Lean4
@[ext]
theorem ext ⦃inst₁ inst₂ : NonUnitalNonAssocRing R⦄ (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
(h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : inst₁ = inst₂ := by
-- Split into `AddCommGroup` instance, `mul` function and properties.
rcases inst₁ with @⟨_, ⟨⟩⟩; rcases inst₂ with @⟨_, ⟨⟩⟩
congr; (ext : 1; assumption)
