English
Two NonUnitalCommSemiring structures on R are equal if their additive and multiplicative components match via the forgetful map.
Русский
Две структуры NonUnitalCommSemiring на R равны, если их аддитивная и мультипликативная части соответствуют друг другу через забывающее отображение.
LaTeX
$$$\\\\forall A,B \\,\\in \\, \\text{NonUnitalCommSemiring}(R), \\\\ toNonUnitalSemiring(A) = toNonUnitalSemiring(B) \\\\Rightarrow A = B.$$$
Lean4
@[ext]
theorem ext ⦃inst₁ inst₂ : NonUnitalCommSemiring R⦄ (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
(h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : inst₁ = inst₂ :=
toNonUnitalSemiring_injective <| NonUnitalSemiring.ext h_add h_mul
