# mathlib3documentation

algebra.big_operators.pi

# Big operators for Pi Types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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)) :
l.sum a = (list.map (λ (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 (λ (f : Π (a : α), β a), f a) l).prod
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) :
s.sum (λ (c : γ), g c) a = s.sum (λ (c : γ), 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) :
s.prod (λ (c : γ), g c) a = s.prod (λ (c : γ), 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) :
s.sum (λ (c : γ), g c) = λ (a : α), s.sum (λ (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 : α), comm_monoid (β a)] (s : finset γ) (g : γ Π (a : α), β a) :
s.prod (λ (c : γ), g c) = λ (a : α), s.prod (λ (c : γ), 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) :
finset.univ.sum (λ (c : γ), g c) a = finset.univ.sum (λ (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) :
finset.univ.prod (λ (c : γ), g c) a = finset.univ.prod (λ (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 : γ β) :
(s.prod (λ (x : γ), f x), s.prod (λ (x : γ), g x)) = s.prod (λ (x : γ), (f x, g x))
theorem prod_mk_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : finset γ) (f : γ α) (g : γ β) :
(s.sum (λ (x : γ), f x), s.sum (λ (x : γ), g x)) = s.sum (λ (x : γ), (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) :
finset.univ.sum (λ (i : I), (f i)) = f
theorem finset.univ_prod_mul_single {I : Type u_1} [decidable_eq I] {Z : I Type u_2} [Π (i : I), comm_monoid (Z i)] [fintype I] (f : Π (i : I), Z i) :
finset.univ.prod (λ (i : I), (f i)) = f
theorem monoid_hom.functions_ext {I : Type u_1} [decidable_eq I] {Z : I Type u_2} [Π (i : I), comm_monoid (Z i)] [finite I] (G : Type u_3) [comm_monoid G] (g h : (Π (i : I), Z i) →* G) (H : (i : I) (x : Z i), g x) = h x)) :
g = h
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)] [finite I] (G : Type u_3) (g h : (Π (i : I), Z i) →+ G) (H : (i : I) (x : Z i), g x) = h 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)] [finite I] (M : Type u_3) (g h : (Π (i : I), Z i) →+ M) (H : (i : I), g.comp = h.comp ) :
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].

@[ext]
theorem monoid_hom.functions_ext' {I : Type u_1} [decidable_eq I] {Z : I Type u_2} [Π (i : I), comm_monoid (Z i)] [finite I] (M : Type u_3) [comm_monoid M] (g h : (Π (i : I), Z i) →* M) (H : (i : I), g.comp i) = h.comp i)) :
g = h

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

@[ext]
theorem ring_hom.functions_ext {I : Type u_1} [decidable_eq I] {f : I Type u_2} [Π (i : I), non_assoc_semiring (f i)] [finite I] (G : Type u_3) (g h : (Π (i : I), f i) →+* G) (H : (i : I) (x : f i), g x) = h x)) :
g = h
theorem prod.fst_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [comm_monoid α] [comm_monoid β] {s : finset γ} {f : γ α × β} :
(s.prod (λ (c : γ), f c)).fst = s.prod (λ (c : γ), (f c).fst)
theorem prod.fst_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : finset γ} {f : γ α × β} :
(s.sum (λ (c : γ), f c)).fst = s.sum (λ (c : γ), (f c).fst)
theorem prod.snd_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [comm_monoid α] [comm_monoid β] {s : finset γ} {f : γ α × β} :
(s.prod (λ (c : γ), f c)).snd = s.prod (λ (c : γ), (f c).snd)
theorem prod.snd_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : finset γ} {f : γ α × β} :
(s.sum (λ (c : γ), f c)).snd = s.sum (λ (c : γ), (f c).snd)