sum_apply — Mathlib

English

For f: α → M and g: α → M → Finsupp β N, and a₂, the value of f.sum g at a₂ equals the sum over i of g i fi a₂.

Русский

Для f и g, значение (f.sum g) в a₂ равно сумме по i от g i (f i) a₂.

LaTeX

$$$$ (f.sum g) a_2 = \\sum_{i} g i (f i) a_2 $$$$

Lean4

@[simp]
theorem sum_apply [Zero M] [AddCommMonoid N] {f : α →₀ M} {g : α → M → β →₀ N} {a₂ : β} :
    (f.sum g) a₂ = f.sum fun a₁ b => g a₁ b a₂ :=
  finset_sum_apply _ _ _

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