instSMul — Mathlib

English

The incidence algebra SMul instance defines a natural action of IncidenceAlgebra 𝕜 α on IncidenceAlgebra 𝕝 α by (f • g)(a,b) = sum_{x∈Icc(a,b)} f(a,x) • g(x,b).

Русский

Инцидентная алгебра обеспечивает естественное действие над IncidenceAlgebra 𝕜 α на IncidenceAlgebra 𝕝 α: (f • g)(a,b) = ∑_{x∈Icc(a,b)} f(a,x) • g(x,b).

LaTeX

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

Lean4

instance instSMul : SMul (IncidenceAlgebra 𝕜 α) (IncidenceAlgebra 𝕝 α) :=
  ⟨fun 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]⟩⟩

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