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 • 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 • 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 => p.fst • p.snd) (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.fst • g p.snd

theorem Finset.cast_card {α : Type u_1} {R : Type u_3} [CommSemiring R] (s : Finset α) : ↑(Finset.card s) = Finset.sum s fun a => 1