mathlib documentation

group_theory.group_action.big_operators

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} [monoid α] [add_monoid β] [distrib_mul_action α β] {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} [monoid α] [add_comm_monoid β] [distrib_mul_action α β] {r : α} {s : multiset β} :
theorem finset.smul_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [monoid α] [add_comm_monoid β] [distrib_mul_action α β] {r : α} {f : γ → β} {s : finset γ} :
r ∑ (x : γ) in s, f x = ∑ (x : γ) in s, r f x
theorem multiset.smul_prod {α : Type u_1} {β : Type u_2} [monoid α] [comm_monoid β] [mul_distrib_mul_action α β] {r : α} {s : multiset β} :
theorem finset.smul_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [monoid α] [comm_monoid β] [mul_distrib_mul_action α β] {r : α} {f : γ → β} {s : finset γ} :
r ∏ (x : γ) in s, f x = ∏ (x : γ) in s, r f x