ext — Mathlib

English

Extensionality for NonUnitalSemiring: equality of Add and Mul parts implies equality of the whole structure.

Русский

Extensionality для NonUnitalSemiring: равенство частей сложения и умножения влечёт равенство всей структуры.

LaTeX

$$$ \text{ext } (h\_add) (h\_mul) \Rightarrow inst = inst' $$$

Lean4

@[ext]
theorem ext ⦃inst₁ inst₂ : NonUnitalSemiring R⦄ (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂])
    (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : inst₁ = inst₂ :=
  toNonUnitalNonAssocSemiring_injective <| NonUnitalNonAssocSemiring.ext h_add h_mul

Похожие утверждения