Lemmas about group actions on big operators

This file contains results about two kinds of actions:

• sums over DistribSMul: r • ∑ x ∈ s, f x = ∑ x ∈ s, r • f x
• products over MulDistribMulAction (with primed name): r • ∏ x ∈ s, f x = ∏ x ∈ s, r • f x
• products over SMulCommClass (with unprimed name): b ^ s.card • ∏ x in s, f x = ∏ x in s, b • f x

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 • ∑ x ∈ s, f x = ∑ x ∈ s, 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 • ∏ x ∈ s, f x = ∏ x ∈ s, r • f x

theorem smul_finprod' {α : Type u_1} {β : Type u_2} [Monoid α] [CommMonoid β] [MulDistribMulAction α β] {ι : Sort u_4} [Finite ι] {f : ι → β} (r : α) : r • ∏ᶠ (x : ι), f x = ∏ᶠ (x : ι), r • f x

theorem Finset.smul_prod_perm {β : Type u_2} [CommMonoid β] {G : Type u_4} [Group G] [MulDistribMulAction G β] [Fintype G] (b : β) (g : G) : g • ∏ h : G, h • b = ∏ h : G, h • b

theorem smul_finprod_perm {β : Type u_2} [CommMonoid β] {G : Type u_4} [Group G] [MulDistribMulAction G β] [Finite G] (b : β) (g : G) : g • ∏ᶠ (h : G), h • b = ∏ᶠ (h : G), h • b

theorem List.smul_prod {α : Type u_1} {β : Type u_2} [Monoid α] [Monoid β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (l : List β) (m : α) : m ^ l.length • l.prod = (List.map (fun (x : β) => m • x) l).prod

theorem List.vadd_sum {α : Type u_1} {β : Type u_2} [AddMonoid α] [AddMonoid β] [AddAction α β] [VAddAssocClass α β β] [VAddCommClass α β β] (l : List β) (m : α) : l.length • m +ᵥ l.sum = (List.map (fun (x : β) => m +ᵥ x) l).sum

theorem Multiset.smul_prod {α : Type u_1} {β : Type u_2} [Monoid α] [CommMonoid β] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (s : Multiset β) (b : α) : b ^ Multiset.card s • s.prod = (Multiset.map (fun (x : β) => b • x) s).prod

theorem Multiset.vadd_sum {α : Type u_1} {β : Type u_2} [AddMonoid α] [AddCommMonoid β] [AddAction α β] [VAddAssocClass α β β] [VAddCommClass α β β] (s : Multiset β) (b : α) : Multiset.card s • b +ᵥ s.sum = (Multiset.map (fun (x : β) => b +ᵥ x) s).sum

theorem Finset.smul_prod {α : Type u_1} {β : Type u_2} [CommMonoid β] [Monoid α] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (s : Finset β) (b : α) (f : β → β) : b ^ s.card • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x

theorem Finset.prod_smul {α : Type u_1} {β : Type u_2} [CommMonoid β] [CommMonoid α] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β] (s : Finset β) (b : β → α) (f : β → β) : ∏ i ∈ s, b i • f i = (∏ i ∈ s, b i) • ∏ i ∈ s, f i