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 = (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 = (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 = (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} : (∑ i ∈ s, f i) • x = ∑ i ∈ s, 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} : (∑ i ∈ s, f i) • ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, 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} [NonAssocSemiring R] (s : Finset α) : ↑s.card = ∑ x ∈ s, 1

theorem Fintype.sum_piFinset_apply {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [DecidableEq ι] [Fintype ι] [AddCommMonoid α] (f : κ → α) (s : Finset κ) (i : ι) : ∑ g ∈ piFinset fun (x : ι) => s, f (g i) = s.card ^ (card ι - 1) • ∑ b ∈ s, f b

@[simp]

theorem Fintype.sum_single_smul {ι : Type u_1} {α : Type u_3} [DecidableEq ι] [Fintype ι] [AddCommMonoid α] {R : Type u_7} [Semiring R] [Module R α] (f : ι → α) (r : R) (i₀ : ι) : ∑ i : ι, Pi.single i₀ r i • f i = r • f i₀