Documentation

Mathlib.Algebra.Module.BigOperators

Finite sums over modules over a ring #

theorem List.sum_smul {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {l : List R} {x : M} :
List.sum l x = List.sum (List.map (fun (r : R) => r x) l)
theorem Multiset.sum_smul {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {l : Multiset R} {x : M} :
Multiset.sum l x = Multiset.sum (Multiset.map (fun (r : R) => r x) l)
theorem Multiset.sum_smul_sum {R : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Multiset R} {t : Multiset M} :
Multiset.sum s Multiset.sum t = Multiset.sum (Multiset.map (fun (p : R × M) => p.1 p.2) (s ×ˢ t))
theorem Finset.sum_smul {R : Type u_3} {M : Type u_4} {ι : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {f : ιR} {s : Finset ι} {x : M} :
(Finset.sum s fun (i : ι) => f i) x = Finset.sum s fun (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] [AddCommMonoid M] [Module R M] {f : αR} {g : βM} {s : Finset α} {t : Finset β} :
((Finset.sum s fun (i : α) => f i) Finset.sum t fun (i : β) => g i) = Finset.sum (s ×ˢ t) fun (p : α × β) => f p.1 g p.2
theorem Finset.cast_card {α : Type u_1} {R : Type u_3} [CommSemiring R] (s : Finset α) :
s.card = Finset.sum s fun (a : α) => 1