Lemmas about group actions on big operators

Note that analogous lemmas for Modules like Finset.sum_smul appear in other files.

theorem List.smul_sum {α : Type u_1} {β : Type u_2} [AddMonoid β] [DistribSMul α β] {r : α} {l : List β} : r • l.sum = (List.map (fun (x : β) => r • x) l).sum

theorem List.smul_prod {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] [MulDistribMulAction α β] {r : α} {l : List β} : r • l.prod = (List.map (fun (x : β) => r • x) l).prod

theorem Multiset.smul_sum {α : Type u_1} {β : Type u_2} [AddCommMonoid β] [DistribSMul α β] {r : α} {s : Multiset β} : r • s.sum = (Multiset.map (fun (x : β) => r • x) s).sum

theorem Finset.smul_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid β] [DistribSMul α β] {r : α} {f : γ → β} {s : Finset γ} : (r • s.sum fun (x : γ) => f x) = s.sum fun (x : γ) => r • f x

theorem Multiset.smul_prod {α : Type u_1} {β : Type u_2} [Monoid α] [CommMonoid β] [MulDistribMulAction α β] {r : α} {s : Multiset β} : r • s.prod = (Multiset.map (fun (x : β) => r • x) s).prod

theorem Finset.smul_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Monoid α] [CommMonoid β] [MulDistribMulAction α β] {r : α} {f : γ → β} {s : Finset γ} : (r • s.prod fun (x : γ) => f x) = s.prod fun (x : γ) => r • f x