English
Two Semiring structures on R are equal if their underlying NonUnitalSemiring, NonAssocSemiring, and MonoidWithZero components align appropriately.
Русский
Две структуры Semiring на R равны, если согласованы соответствующие подструктуры.
LaTeX
$$$\\\\forall A,B \\,\\in \\, \\text{Semiring}(R), \\\\ A{\\\\:}\\\\text{toNonUnitalSemiring} = B{\\\\:}\\\\text{toNonUnitalSemiring} \\\\land A{\\\\:}\\\\text{toNonAssocSemiring} = B{\\\\:}\\\\text{toNonAssocSemiring} \\\\Rightarrow A=B.$$$
Lean4
@[ext]
theorem ext ⦃inst₁ inst₂ : Semiring R⦄ (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
(h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : inst₁ = inst₂ := by
-- Show that enough substructures are equal.
have h₁ : inst₁.toNonUnitalSemiring = inst₂.toNonUnitalSemiring := by ext : 1 <;> assumption
have h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring := by ext : 1 <;> assumption
have h₃ : (inst₁.toMonoidWithZero).toMonoid = (inst₂.toMonoidWithZero).toMonoid := by ext : 1; exact h_mul
cases inst₁; cases inst₂
congr <;>
solve
| injection h₁
| injection h₂
| injection h₃
