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
theorem finsupp.sum_mul {α : Type u_1} {R : Type u_7} {S : Type u_8} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] (b : S) (s : α →₀ R) {f : α → R → S} :
(s.sum f) * b = s.sum (λ (a : α) (c : R), (f a c) * b)
theorem finsupp.mul_sum {α : Type u_1} {R : Type u_7} {S : Type u_8} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] (b : S) (s : α →₀ R) {f : α → R → S} :
b * s.sum f = s.sum (λ (a : α) (c : R), b * f a c)