instMul — Mathlib

English

The incidence algebra is equipped with a convolution-like multiplication: (f*g)(a,b) = sum_{x in [a,b]} f(a,x) g(x,b).

Русский

Инцидентная алгебра обладает умножением, аналогичным свёртке: (f*g)(a,b) = ∑_{x∈[a,b]} f(a,x) g(x,b).

LaTeX

$$$ (f * g) a b = \sum_{x \in Icc\, a b} f a x \; g x b $$$

Lean4

/-- The multiplication operation in incidence algebras is defined on an interval by summing over
all divisions into two subintervals the product of the values of the original pair of functions.
-/
instance instMul : Mul (IncidenceAlgebra 𝕜 α) where
  mul f g := ⟨fun a b ↦ ∑ x ∈ Icc a b, f a x * g x b, fun a b h ↦ by dsimp; rw [Icc_eq_empty h, sum_empty]⟩

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