mathlib documentation

algebra.big_operators.pi

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)) :
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) :
(∑ (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

@[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

@[simp]
theorem add_monoid_hom.finset_sum_apply {ι : Type u_1} {M : Type u_2} {N : Type u_3} [add_monoid M] [add_comm_monoid N] (f : ι → M →+ N) (s : finset ι) (a : M) :
(∑ (i : ι) in s, f i) a = ∑ (i : ι) in s, (f i) a

@[simp]
theorem monoid_hom.finset_prod_apply {ι : Type u_1} {M : Type u_2} {N : Type u_3} [monoid M] [comm_monoid N] (f : ι → M →* N) (s : finset ι) (a : M) :
(∏ (i : ι) in s, f i) a = ∏ (i : ι) in s, (f i) 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) :
∑ (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) :
(∀ (i : I) (x : Z i), g (pi.single i x) = h (pi.single i x))g = h

@[ext]
theorem ring_hom.functions_ext {I : Type u_1} [decidable_eq I] {f : I → Type u_2} [Π (i : I), semiring (f i)] [fintype I] (G : Type u_3) [semiring G] (g h : (Π (i : I), f i) →+* G) :
(∀ (i : I) (x : f i), g (pi.single i x) = h (pi.single i x))g = h

theorem prod.fst_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [comm_monoid α] [comm_monoid β] {s : finset γ} {f : γ → α × β} :
(∏ (c : γ) in s, f c).fst = ∏ (c : γ) in s, (f c).fst

theorem prod.fst_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {s : finset γ} {f : γ → α × β} :
(∑ (c : γ) in s, f c).fst = ∑ (c : γ) in s, (f c).fst

theorem prod.snd_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [comm_monoid α] [comm_monoid β] {s : finset γ} {f : γ → α × β} :
(∏ (c : γ) in s, f c).snd = ∏ (c : γ) in s, (f c).snd

theorem prod.snd_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_comm_monoid α] [add_comm_monoid β] {s : finset γ} {f : γ → α × β} :
(∑ (c : γ) in s, f c).snd = ∑ (c : γ) in s, (f c).snd