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.
theorem
Multiset.smul_sum
{M : Type u_1}
{N : Type u_2}
[AddCommMonoid N]
[DistribSMul M N]
{r : M}
{s : Multiset N}
:
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 γ}
:
theorem
Multiset.smul_prod'
{M : Type u_1}
{N : Type u_2}
[Monoid M]
[CommMonoid N]
[MulDistribMulAction M N]
{r : M}
{s : Multiset N}
:
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 γ}
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
: