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_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 xs, f x = xs, 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 xs, f x = xs, r f x