English
Two CommSemiring structures on the same type are equal if their addition and multiplication operations coincide.
Русский
Две структуры CommSemiring на одном множестве равны, если совпадают операции сложения и умножения.
LaTeX
$$$\\forall R\\, \\forall I_1,I_2:\\, \\text{CommSemiring}(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₂ : CommSemiring R⦄ (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
(h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : inst₁ = inst₂ :=
toSemiring_injective <| Semiring.ext h_add h_mul
