Big operators for Pi Types
This file contains theorems relevant to big operators in binary and arbitrary product of monoids and groups
theorem
pi.list_sum_apply
{α : Type u_1}
{β : α → Type u_2}
[Π (a : α), add_monoid (β a)]
(a : α)
(l : list (Π (a : α), β a)) :
theorem
pi.multiset_sum_apply
{α : Type u_1}
{β : α → Type u_2}
[Π (a : α), add_comm_monoid (β a)]
(a : α)
(s : multiset (Π (a : α), β a)) :
s.sum a = (multiset.map (λ (f : Π (a : α), β a), f a) s).sum
theorem
pi.multiset_prod_apply
{α : Type u_1}
{β : α → Type u_2}
[Π (a : α), comm_monoid (β a)]
(a : α)
(s : multiset (Π (a : α), β a)) :
s.prod a = (multiset.map (λ (f : Π (a : α), β a), f a) s).prod
@[simp]
theorem
finset.prod_apply
{α : Type u_1}
{β : α → Type u_2}
{γ : Type u_3}
[Π (a : α), comm_monoid (β a)]
(a : α)
(s : finset γ)
(g : γ → Π (a : α), β a) :
@[simp]
theorem
finset.sum_apply
{α : Type u_1}
{β : α → Type u_2}
{γ : Type u_3}
[Π (a : α), add_comm_monoid (β a)]
(a : α)
(s : finset γ)
(g : γ → Π (a : α), β a) :
theorem
prod_mk_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[add_comm_monoid β]
(s : finset γ)
(f : γ → α)
(g : γ → β) :
theorem
prod_mk_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[comm_monoid α]
[comm_monoid β]
(s : finset γ)
(f : γ → α)
(g : γ → β) :
theorem
finset.univ_sum_single
{I : Type u_1}
[decidable_eq I]
{Z : I → Type u_2}
[Π (i : I), add_comm_monoid (Z i)]
[fintype I]
(f : Π (i : I), Z i) :
finset.univ.sum (λ (i : I), pi.single i (f i)) = f
@[ext]
theorem
add_monoid_hom.functions_ext
{I : Type u_1}
[decidable_eq I]
{Z : I → Type u_2}
[Π (i : I), add_comm_monoid (Z i)]
[fintype I]
(G : Type u_3)
[add_comm_monoid G]
(g h : (Π (i : I), Z i) →+ G) :
theorem
prod.fst_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[comm_monoid α]
[comm_monoid β]
{s : finset γ}
{f : γ → α × β} :
theorem
prod.fst_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[add_comm_monoid β]
{s : finset γ}
{f : γ → α × β} :
theorem
prod.snd_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[comm_monoid α]
[comm_monoid β]
{s : finset γ}
{f : γ → α × β} :
theorem
prod.snd_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[add_comm_monoid β]
{s : finset γ}
{f : γ → α × β} :