Documentation

Mathlib.Algebra.Module.BigOperators

Finite sums over modules over a ring #

theorem List.sum_smul {R : Type u_5} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {l : List R} {x : M} :
l.sum x = (List.map (fun (r : R) => r x) l).sum
theorem Multiset.sum_smul {R : Type u_5} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {l : Multiset R} {x : M} :
l.sum x = (Multiset.map (fun (r : R) => r x) l).sum
theorem Multiset.sum_smul_sum {R : Type u_5} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {s : Multiset R} {t : Multiset M} :
s.sum t.sum = (Multiset.map (fun (p : R × M) => p.1 p.2) (s ×ˢ t)).sum
theorem Finset.sum_smul {ι : Type u_1} {R : Type u_5} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {f : ιR} {s : Finset ι} {x : M} :
(∑ is, f i) x = is, f i x
theorem Finset.sum_smul_sum {α : Type u_3} {β : Type u_4} {R : Type u_5} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (s : Finset α) (t : Finset β) {f : αR} {g : βM} :
(∑ is, f i) jt, g j = is, jt, f i g j
theorem Fintype.sum_smul_sum {α : Type u_3} {β : Type u_4} {R : Type u_5} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype α] [Fintype β] (f : αR) (g : βM) :
(∑ i : α, f i) j : β, g j = i : α, j : β, f i g j
theorem Finset.cast_card {α : Type u_3} {R : Type u_5} [CommSemiring R] (s : Finset α) :
s.card = as, 1
theorem Fintype.sum_piFinset_apply {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [DecidableEq ι] [Fintype ι] [AddCommMonoid α] (f : κα) (s : Finset κ) (i : ι) :
gFintype.piFinset fun (x : ι) => s, f (g i) = s.card ^ (Fintype.card ι - 1) bs, f b