finset_sum_apply — Mathlib

English

For Finset s and g : α → DFinsupp, the i-th coefficient of the finite sum equals the finite sum of i-th coefficients.

Русский

Для Finset s и g : α → DFinsupp, i-й коэффициент конечной суммы равен сумме i-й коэффициентов.

LaTeX

$$$\\left(\\sum_{a \\in s} g(a)\\right)\\! i = \\sum_{a \\in s} (g(a))\\! i$$$

Lean4

@[simp]
theorem finset_sum_apply {α} [∀ i, AddCommMonoid (β i)] (s : Finset α) (g : α → Π₀ i, β i) (i : ι) :
    (∑ a ∈ s, g a) i = ∑ a ∈ s, g a i :=
  map_sum (evalAddMonoidHom i) g s

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