English
Two NonUnitalNonAssocCommRing structures on the same underlying type are equal if their addition and multiplication operations coincide.
Русский
Две структуры кольца без единицы без ассоциации и коммутативного умножения на одной и той же устойчивой множестве равны, если операции сложения и умножения у них совпадают.
LaTeX
$$$\\forall R\\, \\forall I_1,I_2:\\, \\text{NonUnitalNonAssocCommRing}(R),\\quad (local\\_hAdd[R,I_1] = local\\_hAdd[R,I_2]) \\land (local\\_hMul[R,I_1] = local\\_hMul[R,I_2]) \\Rightarrow I_1 = I_2$$$
Lean4
@[ext]
theorem ext ⦃inst₁ inst₂ : NonUnitalNonAssocCommRing R⦄ (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
(h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : inst₁ = inst₂ :=
toNonUnitalNonAssocRing_injective <| NonUnitalNonAssocRing.ext h_add h_mul
