mathlib3 documentation

algebra.module.big_operators

Finite sums over modules over a ring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem list.sum_smul {R : Type u_3} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {l : list R} {x : M} :
l.sum x = (list.map (λ (r : R), r x) l).sum
theorem multiset.sum_smul {R : Type u_3} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {l : multiset R} {x : M} :
l.sum x = (multiset.map (λ (r : R), r x) l).sum
theorem multiset.sum_smul_sum {R : Type u_3} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {s : multiset R} {t : multiset M} :
s.sum t.sum = (multiset.map (λ (p : R × M), p.fst p.snd) (s ×ˢ t)).sum
theorem finset.sum_smul {R : Type u_3} {M : Type u_4} {ι : Type u_5} [semiring R] [add_comm_monoid M] [module R M] {f : ι R} {s : finset ι} {x : M} :
s.sum (λ (i : ι), f i) x = s.sum (λ (i : ι), f i x)
theorem finset.sum_smul_sum {α : Type u_1} {β : Type u_2} {R : Type u_3} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {f : α R} {g : β M} {s : finset α} {t : finset β} :
s.sum (λ (i : α), f i) t.sum (λ (i : β), g i) = (s ×ˢ t).sum (λ (p : α × β), f p.fst g p.snd)
theorem finset.cast_card {α : Type u_1} {R : Type u_3} [comm_semiring R] (s : finset α) :
(s.card) = s.sum (λ (a : α), 1)