Lemmas about group actions on big operators #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Note that analogous lemmas for modules like finset.sum_smul appear in other files.
theorem
list.smul_sum
{α : Type u_1}
{β : Type u_2}
[add_monoid β]
[distrib_smul α β]
{r : α}
{l : list β} :
theorem
list.smul_prod
{α : Type u_1}
{β : Type u_2}
[monoid α]
[monoid β]
[mul_distrib_mul_action α β]
{r : α}
{l : list β} :
theorem
multiset.smul_sum
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid β]
[distrib_smul α β]
{r : α}
{s : multiset β} :
r • s.sum = (multiset.map (has_smul.smul r) s).sum
theorem
finset.smul_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid β]
[distrib_smul α β]
{r : α}
{f : γ → β}
{s : finset γ} :
theorem
multiset.smul_prod
{α : Type u_1}
{β : Type u_2}
[monoid α]
[comm_monoid β]
[mul_distrib_mul_action α β]
{r : α}
{s : multiset β} :
r • s.prod = (multiset.map (has_smul.smul r) s).prod
theorem
finset.smul_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[monoid α]
[comm_monoid β]
[mul_distrib_mul_action α β]
{r : α}
{f : γ → β}
{s : finset γ} :