# 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 : α) → AddMonoid (β a)] (a : α) (l : List ((a : α) → β a)) :
l.sum a = (List.map (fun (f : (a : α) → β a) => f a) l).sum
theorem Pi.list_prod_apply {α : Type u_1} {β : αType u_2} [(a : α) → Monoid (β a)] (a : α) (l : List ((a : α) → β a)) :
l.prod a = (List.map (fun (f : (a : α) → β a) => f a) l).prod
theorem Pi.multiset_sum_apply {α : Type u_1} {β : αType u_2} [(a : α) → AddCommMonoid (β a)] (a : α) (s : Multiset ((a : α) → β a)) :
s.sum a = (Multiset.map (fun (f : (a : α) → β a) => f a) s).sum
theorem Pi.multiset_prod_apply {α : Type u_1} {β : αType u_2} [(a : α) → CommMonoid (β a)] (a : α) (s : Multiset ((a : α) → β a)) :
s.prod a = (Multiset.map (fun (f : (a : α) → β a) => f a) s).prod
@[simp]
theorem Finset.sum_apply {α : Type u_1} {β : αType u_2} {γ : Type u_3} [(a : α) → AddCommMonoid (β a)] (a : α) (s : ) (g : γ(a : α) → β a) :
s.sum (fun (c : γ) => g c) a = s.sum fun (c : γ) => g c a
@[simp]
theorem Finset.prod_apply {α : Type u_1} {β : αType u_2} {γ : Type u_3} [(a : α) → CommMonoid (β a)] (a : α) (s : ) (g : γ(a : α) → β a) :
s.prod (fun (c : γ) => g c) a = s.prod fun (c : γ) => g c a
theorem Finset.sum_fn {α : Type u_1} {β : αType u_2} {γ : Type u_3} [(a : α) → AddCommMonoid (β a)] (s : ) (g : γ(a : α) → β a) :
(s.sum fun (c : γ) => g c) = fun (a : α) => s.sum fun (c : γ) => g c a

An 'unapplied' analogue of Finset.sum_apply.

theorem Finset.prod_fn {α : Type u_1} {β : αType u_2} {γ : Type u_3} [(a : α) → CommMonoid (β a)] (s : ) (g : γ(a : α) → β a) :
(s.prod fun (c : γ) => g c) = fun (a : α) => s.prod fun (c : γ) => g c a

An 'unapplied' analogue of Finset.prod_apply.

theorem Fintype.sum_apply {α : Type u_1} {β : αType u_2} {γ : Type u_3} [] [(a : α) → AddCommMonoid (β a)] (a : α) (g : γ(a : α) → β a) :
Finset.univ.sum (fun (c : γ) => g c) a = Finset.univ.sum fun (c : γ) => g c a
theorem Fintype.prod_apply {α : Type u_1} {β : αType u_2} {γ : Type u_3} [] [(a : α) → CommMonoid (β a)] (a : α) (g : γ(a : α) → β a) :
Finset.univ.prod (fun (c : γ) => g c) a = Finset.univ.prod fun (c : γ) => g c a
theorem prod_mk_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (s : ) (f : γα) (g : γβ) :
(s.sum fun (x : γ) => f x, s.sum fun (x : γ) => g x) = s.sum fun (x : γ) => (f x, g x)
theorem prod_mk_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] (s : ) (f : γα) (g : γβ) :
(s.prod fun (x : γ) => f x, s.prod fun (x : γ) => g x) = s.prod fun (x : γ) => (f x, g x)
theorem pi_eq_sum_univ {ι : Type u_1} [] [] {R : Type u_2} [] (x : ιR) :
x = Finset.univ.sum fun (i : ι) => x i fun (j : ι) => if i = j then 1 else 0

decomposing x : ι → R as a sum along the canonical basis

theorem Finset.univ_sum_single {I : Type u_1} [] {Z : IType u_2} [(i : I) → AddCommMonoid (Z i)] [] (f : (i : I) → Z i) :
(Finset.univ.sum fun (i : I) => Pi.single i (f i)) = f
theorem Finset.univ_prod_mulSingle {I : Type u_1} [] {Z : IType u_2} [(i : I) → CommMonoid (Z i)] [] (f : (i : I) → Z i) :
(Finset.univ.prod fun (i : I) => Pi.mulSingle i (f i)) = f
theorem AddMonoidHom.functions_ext {I : Type u_1} [] {Z : IType u_2} [(i : I) → AddCommMonoid (Z i)] [] (G : Type u_3) [] (g : ((i : I) → Z i) →+ G) (h : ((i : I) → Z i) →+ G) (H : ∀ (i : I) (x : Z i), g () = h ()) :
g = h
theorem MonoidHom.functions_ext {I : Type u_1} [] {Z : IType u_2} [(i : I) → CommMonoid (Z i)] [] (G : Type u_3) [] (g : ((i : I) → Z i) →* G) (h : ((i : I) → Z i) →* G) (H : ∀ (i : I) (x : Z i), g () = h ()) :
g = h
theorem AddMonoidHom.functions_ext' {I : Type u_1} [] {Z : IType u_2} [(i : I) → AddCommMonoid (Z i)] [] (M : Type u_3) [] (g : ((i : I) → Z i) →+ M) (h : ((i : I) → Z i) →+ M) (H : ∀ (i : I), g.comp () = h.comp ()) :
g = h

This is used as the ext lemma instead of AddMonoidHom.functions_ext for reasons explained in note [partially-applied ext lemmas].

theorem MonoidHom.functions_ext' {I : Type u_1} [] {Z : IType u_2} [(i : I) → CommMonoid (Z i)] [] (M : Type u_3) [] (g : ((i : I) → Z i) →* M) (h : ((i : I) → Z i) →* M) (H : ∀ (i : I), g.comp () = h.comp ()) :
g = h

This is used as the ext lemma instead of MonoidHom.functions_ext for reasons explained in note [partially-applied ext lemmas].

theorem RingHom.functions_ext {I : Type u_1} [] {f : IType u_2} [(i : I) → NonAssocSemiring (f i)] [] (G : Type u_3) [] (g : ((i : I) → f i) →+* G) (h : ((i : I) → f i) →+* G) (H : ∀ (i : I) (x : f i), g () = h ()) :
g = h
theorem Prod.fst_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {s : } {f : γα × β} :
(s.sum fun (c : γ) => f c).1 = s.sum fun (c : γ) => (f c).1
theorem Prod.fst_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {s : } {f : γα × β} :
(s.prod fun (c : γ) => f c).1 = s.prod fun (c : γ) => (f c).1
theorem Prod.snd_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {s : } {f : γα × β} :
(s.sum fun (c : γ) => f c).2 = s.sum fun (c : γ) => (f c).2
theorem Prod.snd_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {s : } {f : γα × β} :
(s.prod fun (c : γ) => f c).2 = s.prod fun (c : γ) => (f c).2