Documentation

Mathlib.Algebra.BigOperators.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 : α) → AddMonoid (β a)] (a : α) (l : List ((a : α) → β a)) :
List.sum ((a : α) → β a) Pi.instAdd Pi.instZero l a = List.sum (List.map (fun f => f a) l)
theorem Pi.list_prod_apply {α : Type u_1} {β : αType u_2} [(a : α) → Monoid (β a)] (a : α) (l : List ((a : α) → β a)) :
List.prod ((a : α) → β a) Pi.instMul Pi.instOne l a = List.prod (List.map (fun f => f a) l)
theorem Pi.multiset_sum_apply {α : Type u_1} {β : αType u_2} [(a : α) → AddCommMonoid (β a)] (a : α) (s : Multiset ((a : α) → β a)) :
Multiset.sum ((a : α) → β a) Pi.addCommMonoid s a = Multiset.sum (Multiset.map (fun f => f a) s)
theorem Pi.multiset_prod_apply {α : Type u_1} {β : αType u_2} [(a : α) → CommMonoid (β a)] (a : α) (s : Multiset ((a : α) → β a)) :
Multiset.prod ((a : α) → β a) Pi.commMonoid s a = Multiset.prod (Multiset.map (fun f => f a) s)
@[simp]
theorem Finset.sum_apply {α : Type u_1} {β : αType u_2} {γ : Type u_3} [(a : α) → AddCommMonoid (β a)] (a : α) (s : Finset γ) (g : γ(a : α) → β a) :
Finset.sum ((a : α) → β a) γ Pi.addCommMonoid s (fun c => g c) a = Finset.sum s fun c => g c a
@[simp]
theorem Finset.prod_apply {α : Type u_1} {β : αType u_2} {γ : Type u_3} [(a : α) → CommMonoid (β a)] (a : α) (s : Finset γ) (g : γ(a : α) → β a) :
Finset.prod ((a : α) → β a) γ Pi.commMonoid s (fun c => g c) a = Finset.prod s fun c => g c a
theorem Finset.sum_fn {α : Type u_1} {β : αType u_2} {γ : Type u_3} [(a : α) → AddCommMonoid (β a)] (s : Finset γ) (g : γ(a : α) → β a) :
(Finset.sum s fun c => g c) = fun a => Finset.sum s 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 : Finset γ) (g : γ(a : α) → β a) :
(Finset.prod s fun c => g c) = fun a => Finset.prod s 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} [Fintype γ] [(a : α) → AddCommMonoid (β a)] (a : α) (g : γ(a : α) → β a) :
Finset.sum ((a : α) → β a) γ Pi.addCommMonoid Finset.univ (fun c => g c) a = Finset.sum Finset.univ fun c => g c a
theorem Fintype.prod_apply {α : Type u_1} {β : αType u_2} {γ : Type u_3} [Fintype γ] [(a : α) → CommMonoid (β a)] (a : α) (g : γ(a : α) → β a) :
Finset.prod ((a : α) → β a) γ Pi.commMonoid Finset.univ (fun c => g c) a = Finset.prod Finset.univ fun c => g c a
theorem prod_mk_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [AddCommMonoid β] (s : Finset γ) (f : γα) (g : γβ) :
(Finset.sum s fun x => f x, Finset.sum s fun x => g x) = Finset.sum s fun x => (f x, g x)
theorem prod_mk_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [CommMonoid β] (s : Finset γ) (f : γα) (g : γβ) :
(Finset.prod s fun x => f x, Finset.prod s fun x => g x) = Finset.prod s fun x => (f x, g x)
theorem Finset.univ_sum_single {I : Type u_1} [DecidableEq I] {Z : IType u_2} [(i : I) → AddCommMonoid (Z i)] [Fintype I] (f : (i : I) → Z i) :
(Finset.sum Finset.univ fun i => Pi.single i (f i)) = f
theorem Finset.univ_prod_mulSingle {I : Type u_1} [DecidableEq I] {Z : IType u_2} [(i : I) → CommMonoid (Z i)] [Fintype I] (f : (i : I) → Z i) :
(Finset.prod Finset.univ fun i => Pi.mulSingle i (f i)) = f
theorem AddMonoidHom.functions_ext {I : Type u_1} [DecidableEq I] {Z : IType u_2} [(i : I) → AddCommMonoid (Z i)] [Finite I] (G : Type u_3) [AddCommMonoid G] (g : ((i : I) → Z i) →+ G) (h : ((i : I) → Z i) →+ G) (H : ∀ (i : I) (x : Z i), g (Pi.single i x) = h (Pi.single i x)) :
g = h
theorem MonoidHom.functions_ext {I : Type u_1} [DecidableEq I] {Z : IType u_2} [(i : I) → CommMonoid (Z i)] [Finite I] (G : Type u_3) [CommMonoid G] (g : ((i : I) → Z i) →* G) (h : ((i : I) → Z i) →* G) (H : ∀ (i : I) (x : Z i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)) :
g = h
theorem AddMonoidHom.functions_ext' {I : Type u_1} [DecidableEq I] {Z : IType u_2} [(i : I) → AddCommMonoid (Z i)] [Finite I] (M : Type u_3) [AddCommMonoid M] (g : ((i : I) → Z i) →+ M) (h : ((i : I) → Z i) →+ M) (H : ∀ (i : I), AddMonoidHom.comp g (AddMonoidHom.single Z i) = AddMonoidHom.comp h (AddMonoidHom.single Z i)) :
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} [DecidableEq I] {Z : IType u_2} [(i : I) → CommMonoid (Z i)] [Finite I] (M : Type u_3) [CommMonoid M] (g : ((i : I) → Z i) →* M) (h : ((i : I) → Z i) →* M) (H : ∀ (i : I), MonoidHom.comp g (MonoidHom.single Z i) = MonoidHom.comp h (MonoidHom.single Z i)) :
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} [DecidableEq I] {f : IType u_2} [(i : I) → NonAssocSemiring (f i)] [Finite I] (G : Type u_3) [NonAssocSemiring G] (g : ((i : I) → f i) →+* G) (h : ((i : I) → f i) →+* G) (H : ∀ (i : I) (x : f i), g (Pi.single i x) = h (Pi.single i x)) :
g = h
theorem Prod.fst_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {s : Finset γ} {f : γα × β} :
(Finset.sum s fun c => f c).fst = Finset.sum s fun c => (f c).fst
theorem Prod.fst_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [CommMonoid β] {s : Finset γ} {f : γα × β} :
(Finset.prod s fun c => f c).fst = Finset.prod s fun c => (f c).fst
theorem Prod.snd_sum {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [AddCommMonoid β] {s : Finset γ} {f : γα × β} :
(Finset.sum s fun c => f c).snd = Finset.sum s fun c => (f c).snd
theorem Prod.snd_prod {α : Type u_1} {β : Type u_2} {γ : Type u_3} [CommMonoid α] [CommMonoid β] {s : Finset γ} {f : γα × β} :
(Finset.prod s fun c => f c).snd = Finset.prod s fun c => (f c).snd