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_1} {ι : Type u_2} {A : Type u_4} [add_comm_monoid A] {s : finset α} {f : α → ι →₀ A} (i : ι) :
(∑ (k : α) in s, f k) i = ∑ (k : α) in s, (f k) i

theorem finsupp.sum_apply' {ι : Type u_2} {γ : Type u_3} {A : Type u_4} {B : Type u_5} [add_comm_monoid A] [add_comm_monoid B] (g : ι →₀ A) (k : ι → A → γ → B) (x : γ) :
g.sum k x = g.sum (λ (i : ι) (b : A), k i b x)

theorem finsupp.sum_sum_index' {α : Type u_1} {ι : Type u_2} {A : Type u_4} {C : Type u_6} [add_comm_monoid A] [add_comm_monoid C] {t : ι → A → C} (h0 : ∀ (i : ι), t i 0 = 0) (h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y) {s : finset α} {f : α → ι →₀ A} :
(∑ (x : α) in s, f x).sum t = ∑ (x : α) in s, (f x).sum t