# 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 ∈ s, f x = ∏ x ∈ s, b • f x`

Note that analogous lemmas for `Module`s like `Finset.sum_smul` appear in other files.

source
theorem List.smul_sum {M : Type u_1} {N : Type u_2} [AddMonoid N] [DistribSMul M N] {r : M} {l : List N} :
r • l.sum = (map (fun (x : N) => r • x) l).sum
source
theorem List.smul_prod' {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] [MulDistribMulAction M N] {r : M} {l : List N} :
r • l.prod = (map (fun (x : N) => r • x) l).prod
source
theorem Multiset.smul_sum {M : Type u_1} {N : Type u_2} [AddCommMonoid N] [DistribSMul M N] {r : M} {s : Multiset N} :
r • s.sum = (map (fun (x : N) => r • x) s).sum
source
theorem Finset.smul_sum {M : Type u_1} {N : Type u_2} {γ : Type u_3} [AddCommMonoid N] [DistribSMul M N] {r : M} {f : γ → N} {s : Finset γ} :
r • ∑ x ∈ s, f x = ∑ x ∈ s, r • f x
source
theorem smul_finsum_mem {M : Type u_1} {N : Type u_2} {γ : Type u_3} [AddCommMonoid N] [DistribSMul M N] {r : M} {f : γ → N} {s : Set γ} (hs : s.Finite) :
r • ∑ᶠ (x : γ) (_ : x ∈ s), f x = ∑ᶠ (x : γ) (_ : x ∈ s), r • f x
source
theorem Multiset.smul_prod' {M : Type u_1} {N : Type u_2} [Monoid M] [CommMonoid N] [MulDistribMulAction M N] {r : M} {s : Multiset N} :
r • s.prod = (map (fun (x : N) => r • x) s).prod
source
theorem Finset.smul_prod' {M : Type u_1} {N : Type u_2} {γ : Type u_3} [Monoid M] [CommMonoid N] [MulDistribMulAction M N] {r : M} {f : γ → N} {s : Finset γ} :
r • ∏ x ∈ s, f x = ∏ x ∈ s, r • f x
source
theorem smul_finprod' {M : Type u_1} {N : Type u_2} [Monoid M] [CommMonoid N] [MulDistribMulAction M N] {ι : Sort u_4} [Finite ι] {f : ι → N} (r : M) :
r • ∏ᶠ (x : ι), f x = ∏ᶠ (x : ι), r • f x
source
theorem Finset.smul_prod_perm {N : Type u_2} [CommMonoid N] {G : Type u_4} [Group G] [MulDistribMulAction G N] [Fintype G] (b : N) (g : G) :
g • ∏ h : G, h • b = ∏ h : G, h • b
source
theorem smul_finprod_perm {N : Type u_2} [CommMonoid N] {G : Type u_4} [Group G] [MulDistribMulAction G N] [Finite G] (b : N) (g : G) :
g • ∏ᶠ (h : G), h • b = ∏ᶠ (h : G), h • b
source
theorem List.smul_prod {M : Type u_1} {N : Type u_2} [Monoid M] [MulOneClass N] [MulAction M N] [IsScalarTower M N N] [SMulCommClass M N N] (l : List N) (m : M) :
m ^ l.length • l.prod = (map (fun (x : N) => m • x) l).prod
source
theorem List.vadd_sum {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddZeroClass N] [AddAction M N] [VAddAssocClass M N N] [VAddCommClass M N N] (l : List N) (m : M) :
l.length • m +ᵥ l.sum = (map (fun (x : N) => m +ᵥ x) l).sum
source
theorem Multiset.smul_prod {M : Type u_1} {N : Type u_2} [Monoid M] [CommMonoid N] [MulAction M N] [IsScalarTower M N N] [SMulCommClass M N N] (s : Multiset N) (b : M) :
b ^ s.card • s.prod = (map (fun (x : N) => b • x) s).prod
source
theorem Multiset.vadd_sum {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddCommMonoid N] [AddAction M N] [VAddAssocClass M N N] [VAddCommClass M N N] (s : Multiset N) (b : M) :
s.card • b +ᵥ s.sum = (map (fun (x : N) => b +ᵥ x) s).sum
source
theorem Finset.smul_prod {M : Type u_1} {N : Type u_2} [CommMonoid N] [Monoid M] [MulAction M N] [IsScalarTower M N N] [SMulCommClass M N N] (s : Finset N) (b : M) (f : N → N) :
b ^ s.card • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x
source
theorem Finset.prod_smul {M : Type u_1} {N : Type u_2} [CommMonoid N] [CommMonoid M] [MulAction M N] [IsScalarTower M N N] [SMulCommClass M N N] (s : Finset N) (b : N → M) (f : N → N) :
∏ i ∈ s, b i • f i = (∏ i ∈ s, b i) • ∏ i ∈ s, f i