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
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) :
∑ (i : I), pi.single i (f i) = f
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].

@[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) (w : ∀ (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