# Documentation

Mathlib.GroupTheory.GroupAction.BigOperators

# 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_2} {β : Type u_1} [inst : ] [inst : ] {r : α} {l : List β} :
r = List.sum (List.map ((fun x x_1 => x x_1) r) l)
theorem List.smul_prod {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] [inst : ] {r : α} {l : List β} :
r = List.prod (List.map ((fun x x_1 => x x_1) r) l)
theorem Multiset.smul_sum {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] {r : α} {s : } :
= Multiset.sum (Multiset.map ((fun x x_1 => x x_1) r) s)
theorem Finset.smul_sum {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : ] [inst : ] {r : α} {f : γβ} {s : } :
(r Finset.sum s fun x => f x) = Finset.sum s fun x => r f x
theorem Multiset.smul_prod {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] [inst : ] {r : α} {s : } :
= Multiset.prod (Multiset.map ((fun x x_1 => x x_1) r) s)
theorem Finset.smul_prod {α : Type u_3} {β : Type u_2} {γ : Type u_1} [inst : ] [inst : ] [inst : ] {r : α} {f : γβ} {s : } :
(r Finset.prod s fun x => f x) = Finset.prod s fun x => r f x