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.sum_apply
{α : Type u_1}
{β : α → Type u_2}
{γ : Type u_3}
[Π (a : α), add_comm_monoid (β a)]
(a : α)
(s : finset γ)
(g : γ → Π (a : α), β a) :
(∑ (c : γ) in s, g c) a = ∑ (c : γ) in s, g c a
@[simp]
theorem
finset.prod_apply
{α : Type u_1}
{β : α → Type u_2}
{γ : Type u_3}
[Π (a : α), comm_monoid (β a)]
(a : α)
(s : finset γ)
(g : γ → Π (a : α), β a) :
(∏ (c : γ) in s, g c) a = ∏ (c : γ) in s, g c a
theorem
finset.sum_fn
{α : Type u_1}
{β : α → Type u_2}
{γ : Type u_3}
[Π (a : α), add_comm_monoid (β a)]
(s : finset γ)
(g : γ → Π (a : α), β a) :
∑ (c : γ) in s, g c = λ (a : α), ∑ (c : γ) in s, g c a
An 'unapplied' analogue of finset.sum_apply.
theorem
finset.prod_fn
{α : Type u_1}
{β : α → Type u_2}
{γ : Type u_3}
[Π (a : α), comm_monoid (β a)]
(s : finset γ)
(g : γ → Π (a : α), β a) :
∏ (c : γ) in s, g c = λ (a : α), ∏ (c : γ) in s, g c a
An 'unapplied' analogue of finset.prod_apply.
@[simp]
theorem
fintype.sum_apply
{α : Type u_1}
{β : α → Type u_2}
{γ : Type u_3}
[fintype γ]
[Π (a : α), add_comm_monoid (β a)]
(a : α)
(g : γ → Π (a : α), β a) :
(∑ (c : γ), g c) a = ∑ (c : γ), g c a
@[simp]
theorem
fintype.prod_apply
{α : Type u_1}
{β : α → Type u_2}
{γ : Type u_3}
[fintype γ]
[Π (a : α), comm_monoid (β a)]
(a : α)
(g : γ → Π (a : α), β a) :
(∏ (c : γ), g c) a = ∏ (c : γ), g c a
theorem
prod_mk_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[comm_monoid α]
[comm_monoid β]
(s : finset γ)
(f : γ → α)
(g : γ → β) :
(∏ (x : γ) in s, f x, ∏ (x : γ) in s, g x) = ∏ (x : γ) in s, (f x, g x)
theorem
prod_mk_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[add_comm_monoid β]
(s : finset γ)
(f : γ → α)
(g : γ → β) :
(∑ (x : γ) in s, f x, ∑ (x : γ) in s, g x) = ∑ (x : γ) in s, (f x, g x)
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) :
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)
(w : ∀ (i : I) (x : Z i), ⇑g (pi.single i x) = ⇑h (pi.single i x)) :
g = h
@[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]
(M : Type u_3)
[add_comm_monoid M]
(g h : (Π (i : I), Z i) →+ M)
(H : ∀ (i : I), g.comp (add_monoid_hom.single Z i) = h.comp (add_monoid_hom.single Z i)) :
g = h
This is used as the ext lemma instead of add_monoid_hom.functions_ext for reasons explained in
note [partially-applied ext lemmas].
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 : γ → α × β} :