mathlib documentation

algebra.big_operators.finsupp

Big operators for finsupps

This file contains theorems relevant to big operators in finitely supported functions.

theorem finset.sum_apply' {α : Type u} {ι : Type v} {β : Type w} [add_comm_monoid β] {s : finset α} {f : α → ι →₀ β} (i : ι) :
(∑ (k : α) in s, f k) i = ∑ (k : α) in s, (f k) i

theorem finsupp.sum_apply' {ι : Type v} {β : Type w} [add_comm_monoid β] {γ : Type u₁} {δ : Type v₁} [add_comm_monoid δ] (g : ι →₀ β) (k : ι → β → γ → δ) (x : γ) :
g.sum k x = g.sum (λ (i : ι) (b : β), k i b x)

theorem finsupp.sum_sum_index' {α : Type u} {ι : Type v} {β : Type w} [add_comm_monoid β] {s : finset α} {f : α → ι →₀ β} {ε : Type w₁} [add_comm_monoid ε] {t : ι → β → ε} :
(∀ (i : ι), t i 0 = 0)(∀ (i : ι) (x y : β), t i (x + y) = t i x + t i y)(∑ (x : α) in s, f x).sum t = ∑ (x : α) in s, (f x).sum t