instNonUnitalNonAssocSemiring — Mathlib

English

Two incidence-algebra elements are equal if they agree on all comparable pairs.

Русский

Два элемента инцидентной алгебры равны, если их значения совпадают на всех сравнимых парах.

LaTeX

$$∀ {f g : IncidenceAlgebra 𝕜 α} (h : ∀ a b, a ≤ b → f a b = g a b), f = g$$

Lean4

instance instNonUnitalNonAssocSemiring [Preorder α] [LocallyFiniteOrder α] [NonUnitalNonAssocSemiring 𝕜] :
    NonUnitalNonAssocSemiring (IncidenceAlgebra 𝕜 α)
    where
  __ := instAddCommMonoid
  mul := (· * ·)
  zero := 0
  zero_mul := fun f ↦ by ext; exact sum_eq_zero fun x _ ↦ zero_mul _
  mul_zero := fun f ↦ by ext; exact sum_eq_zero fun x _ ↦ mul_zero _
  left_distrib := fun f g h ↦ by ext; exact Eq.trans (sum_congr rfl fun x _ ↦ left_distrib _ _ _) sum_add_distrib
  right_distrib := fun f g h ↦ by ext; exact Eq.trans (sum_congr rfl fun x _ ↦ right_distrib _ _ _) sum_add_distrib

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