English
Equality of two distributive structures is determined by equality of their addition and multiplication operations.
Русский
Равенство двух распределительных структур определяется равенством их сложения и умножения.
LaTeX
$$$ \text{ext } (h_{add}: local_hAdd = local_hAdd') (h_{mul}: local_hMul = local_hMul') \Rightarrow \, inst = inst' $$$
Lean4
@[ext]
theorem ext ⦃inst₁ inst₂ : Distrib 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 `add` and `mul` functions and properties.
rcases inst₁ with @⟨⟨⟩, ⟨⟩⟩
rcases inst₂ with
@⟨⟨⟩, ⟨⟩⟩
-- Prove equality of parts using function extensionality.
congr
