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 • List.sum l = List.sum (List.map ((fun x x_1 => x • x_1) r) l)

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

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

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

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

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