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)