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_prod_apply {α : Type u_4} {β : α → Type u_5} [(a : α) → Monoid (β a)] (a : α) (l : List ((a : α) → β a)) : Eq (l.prod a) (List.map (fun (f : (a : α) → β a) => f a) l).prod

theorem Pi.list_sum_apply {α : Type u_4} {β : α → Type u_5} [(a : α) → AddMonoid (β a)] (a : α) (l : List ((a : α) → β a)) : Eq (l.sum a) (List.map (fun (f : (a : α) → β a) => f a) l).sum

theorem Pi.multiset_prod_apply {α : Type u_4} {β : α → Type u_5} [(a : α) → CommMonoid (β a)] (a : α) (s : Multiset ((a : α) → β a)) : Eq (s.prod a) (Multiset.map (fun (f : (a : α) → β a) => f a) s).prod

theorem Pi.multiset_sum_apply {α : Type u_4} {β : α → Type u_5} [(a : α) → AddCommMonoid (β a)] (a : α) (s : Multiset ((a : α) → β a)) : Eq (s.sum a) (Multiset.map (fun (f : (a : α) → β a) => f a) s).sum

theorem Finset.prod_apply {α : Type u_4} {β : α → Type u_5} {γ : Type u_6} [(a : α) → CommMonoid (β a)] (a : α) (s : Finset γ) (g : γ → (a : α) → β a) : Eq (s.prod (fun (c : γ) => g c) a) (s.prod fun (c : γ) => g c a)

theorem Finset.sum_apply {α : Type u_4} {β : α → Type u_5} {γ : Type u_6} [(a : α) → AddCommMonoid (β a)] (a : α) (s : Finset γ) (g : γ → (a : α) → β a) : Eq (s.sum (fun (c : γ) => g c) a) (s.sum fun (c : γ) => g c a)

theorem Finset.prod_fn {α : Type u_4} {β : α → Type u_5} {γ : Type u_6} [(a : α) → CommMonoid (β a)] (s : Finset γ) (g : γ → (a : α) → β a) : Eq (s.prod fun (c : γ) => g c) fun (a : α) => s.prod fun (c : γ) => g c a

An 'unapplied' analogue of Finset.prod_apply.

theorem Finset.sum_fn {α : Type u_4} {β : α → Type u_5} {γ : Type u_6} [(a : α) → AddCommMonoid (β a)] (s : Finset γ) (g : γ → (a : α) → β a) : Eq (s.sum fun (c : γ) => g c) fun (a : α) => s.sum fun (c : γ) => g c a

An 'unapplied' analogue of Finset.sum_apply.

theorem Fintype.prod_apply {α : Type u_4} {β : α → Type u_5} {γ : Type u_6} [Fintype γ] [(a : α) → CommMonoid (β a)] (a : α) (g : γ → (a : α) → β a) : Eq (Finset.univ.prod (fun (c : γ) => g c) a) (Finset.univ.prod fun (c : γ) => g c a)

theorem Fintype.sum_apply {α : Type u_4} {β : α → Type u_5} {γ : Type u_6} [Fintype γ] [(a : α) → AddCommMonoid (β a)] (a : α) (g : γ → (a : α) → β a) : Eq (Finset.univ.sum (fun (c : γ) => g c) a) (Finset.univ.sum fun (c : γ) => g c a)

theorem prod_mk_prod {α : Type u_4} {β : Type u_5} {γ : Type u_6} [CommMonoid α] [CommMonoid β] (s : Finset γ) (f : γ → α) (g : γ → β) : Eq { fst := s.prod fun (x : γ) => f x, snd := s.prod fun (x : γ) => g x } (s.prod fun (x : γ) => { fst := f x, snd := g x })

theorem prod_mk_sum {α : Type u_4} {β : Type u_5} {γ : Type u_6} [AddCommMonoid α] [AddCommMonoid β] (s : Finset γ) (f : γ → α) (g : γ → β) : Eq { fst := s.sum fun (x : γ) => f x, snd := s.sum fun (x : γ) => g x } (s.sum fun (x : γ) => { fst := f x, snd := g x })

theorem pi_eq_sum_univ {ι : Type u_4} [Fintype ι] [DecidableEq ι] {R : Type u_5} [Semiring R] (x : ι → R) : Eq x (Finset.univ.sum fun (i : ι) => HSMul.hSMul (x i) fun (j : ι) => ite (Eq i j) 1 0)

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

theorem prod_indicator_apply {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [CommSemiring α] (s : Finset ι) (f : ι → Set κ) (g : ι → κ → α) (j : κ) : Eq (s.prod fun (i : ι) => (f i).indicator (g i) j) ((Set.iInter fun (x : ι) => Set.iInter fun (h : Membership.mem s x) => f x).indicator (s.prod fun (i : ι) => g i) j)

theorem prod_indicator {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [CommSemiring α] (s : Finset ι) (f : ι → Set κ) (g : ι → κ → α) : Eq (s.prod fun (i : ι) => (f i).indicator (g i)) ((Set.iInter fun (x : ι) => Set.iInter fun (h : Membership.mem s x) => f x).indicator (s.prod fun (i : ι) => g i))

theorem prod_indicator_const_apply {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [CommSemiring α] (s : Finset ι) (f : ι → Set κ) (g : κ → α) (j : κ) : Eq (s.prod fun (i : ι) => (f i).indicator g j) ((Set.iInter fun (x : ι) => Set.iInter fun (h : Membership.mem s x) => f x).indicator (HPow.hPow g s.card) j)

theorem prod_indicator_const {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [CommSemiring α] (s : Finset ι) (f : ι → Set κ) (g : κ → α) : Eq (s.prod fun (i : ι) => (f i).indicator g) ((Set.iInter fun (x : ι) => Set.iInter fun (h : Membership.mem s x) => f x).indicator (HPow.hPow g s.card))

theorem Finset.univ_prod_mulSingle {I : Type u_4} [DecidableEq I] {Z : I → Type u_5} [(i : I) → CommMonoid (Z i)] [Fintype I] (f : (i : I) → Z i) : Eq (univ.prod fun (i : I) => Pi.mulSingle i (f i)) f

theorem Finset.univ_sum_single {I : Type u_4} [DecidableEq I] {Z : I → Type u_5} [(i : I) → AddCommMonoid (Z i)] [Fintype I] (f : (i : I) → Z i) : Eq (univ.sum fun (i : I) => Pi.single i (f i)) f

theorem MonoidHom.functions_ext {I : Type u_4} [DecidableEq I] {Z : I → Type u_5} [(i : I) → CommMonoid (Z i)] [Finite I] (G : Type u_6) [CommMonoid G] (g h : MonoidHom ((i : I) → Z i) G) (H : ∀ (i : I) (x : Z i), Eq (DFunLike.coe g (Pi.mulSingle i x)) (DFunLike.coe h (Pi.mulSingle i x))) : Eq g h

theorem AddMonoidHom.functions_ext {I : Type u_4} [DecidableEq I] {Z : I → Type u_5} [(i : I) → AddCommMonoid (Z i)] [Finite I] (G : Type u_6) [AddCommMonoid G] (g h : AddMonoidHom ((i : I) → Z i) G) (H : ∀ (i : I) (x : Z i), Eq (DFunLike.coe g (Pi.single i x)) (DFunLike.coe h (Pi.single i x))) : Eq g h

theorem MonoidHom.functions_ext' {I : Type u_4} [DecidableEq I] {Z : I → Type u_5} [(i : I) → CommMonoid (Z i)] [Finite I] (M : Type u_6) [CommMonoid M] (g h : MonoidHom ((i : I) → Z i) M) (H : ∀ (i : I), Eq (g.comp (mulSingle Z i)) (h.comp (mulSingle Z i))) : Eq g h

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

theorem AddMonoidHom.functions_ext' {I : Type u_4} [DecidableEq I] {Z : I → Type u_5} [(i : I) → AddCommMonoid (Z i)] [Finite I] (M : Type u_6) [AddCommMonoid M] (g h : AddMonoidHom ((i : I) → Z i) M) (H : ∀ (i : I), Eq (g.comp (single Z i)) (h.comp (single Z i))) : Eq g h

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

theorem AddMonoidHom.functions_ext'_iff {I : Type u_4} [DecidableEq I] {Z : I → Type u_5} [(i : I) → AddCommMonoid (Z i)] [Finite I] {M : Type u_6} [AddCommMonoid M] {g h : AddMonoidHom ((i : I) → Z i) M} : Iff (Eq g h) (∀ (i : I), Eq (g.comp (single Z i)) (h.comp (single Z i)))

theorem MonoidHom.functions_ext'_iff {I : Type u_4} [DecidableEq I] {Z : I → Type u_5} [(i : I) → CommMonoid (Z i)] [Finite I] {M : Type u_6} [CommMonoid M] {g h : MonoidHom ((i : I) → Z i) M} : Iff (Eq g h) (∀ (i : I), Eq (g.comp (mulSingle Z i)) (h.comp (mulSingle Z i)))

theorem RingHom.functions_ext {I : Type u_4} [DecidableEq I] {f : I → Type u_5} [(i : I) → NonAssocSemiring (f i)] [Finite I] (G : Type u_6) [NonAssocSemiring G] (g h : RingHom ((i : I) → f i) G) (H : ∀ (i : I) (x : f i), Eq (DFunLike.coe g (Pi.single i x)) (DFunLike.coe h (Pi.single i x))) : Eq g h

theorem RingHom.functions_ext_iff {I : Type u_4} [DecidableEq I] {f : I → Type u_5} [(i : I) → NonAssocSemiring (f i)] [Finite I] {G : Type u_6} [NonAssocSemiring G] {g h : RingHom ((i : I) → f i) G} : Iff (Eq g h) (∀ (i : I) (x : f i), Eq (DFunLike.coe g (Pi.single i x)) (DFunLike.coe h (Pi.single i x)))

theorem Prod.fst_prod {α : Type u_4} {β : Type u_5} {γ : Type u_6} [CommMonoid α] [CommMonoid β] {s : Finset γ} {f : γ → Prod α β} : Eq (s.prod fun (c : γ) => f c).fst (s.prod fun (c : γ) => (f c).fst)

theorem Prod.fst_sum {α : Type u_4} {β : Type u_5} {γ : Type u_6} [AddCommMonoid α] [AddCommMonoid β] {s : Finset γ} {f : γ → Prod α β} : Eq (s.sum fun (c : γ) => f c).fst (s.sum fun (c : γ) => (f c).fst)

theorem Prod.snd_prod {α : Type u_4} {β : Type u_5} {γ : Type u_6} [CommMonoid α] [CommMonoid β] {s : Finset γ} {f : γ → Prod α β} : Eq (s.prod fun (c : γ) => f c).snd (s.prod fun (c : γ) => (f c).snd)

theorem Prod.snd_sum {α : Type u_4} {β : Type u_5} {γ : Type u_6} [AddCommMonoid α] [AddCommMonoid β] {s : Finset γ} {f : γ → Prod α β} : Eq (s.sum fun (c : γ) => f c).snd (s.sum fun (c : γ) => (f c).snd)

def Pi.monoidHomMulEquiv {ι : Type u_4} [Fintype ι] [DecidableEq ι] (M : ι → Type u_5) [(i : ι) → CommMonoid (M i)] (M' : Type u_6) [CommMonoid M'] : MulEquiv (MonoidHom ((i : ι) → M i) M') ((i : ι) → MonoidHom (M i) M')

The canonical isomorphism between the monoid of homomorphisms from a finite product of commutative monoids to another commutative monoid and the product of the homomorphism monoids.

Equations

• One or more equations did not get rendered due to their size.

def Pi.addMonoidHomAddEquiv {ι : Type u_4} [Fintype ι] [DecidableEq ι] (M : ι → Type u_5) [(i : ι) → AddCommMonoid (M i)] (M' : Type u_6) [AddCommMonoid M'] : AddEquiv (AddMonoidHom ((i : ι) → M i) M') ((i : ι) → AddMonoidHom (M i) M')

The canonical isomorphism between the additive monoid of homomorphisms from a finite product of additive commutative monoids to another additive commutative monoid and the product of the homomorphism monoids.

Equations

• One or more equations did not get rendered due to their size.

theorem Pi.single_induction {ι : Type u_1} [Finite ι] [DecidableEq ι] {M : Type u_4} [AddCommMonoid M] (p : (ι → M) → Prop) (f : ι → M) (zero : p 0) (add : ∀ (f g : ι → M), p f → p g → p (HAdd.hAdd f g)) (single : ∀ (i : ι) (m : M), p (single i m)) : p f

theorem Pi.mulSingle_induction {ι : Type u_1} [Finite ι] [DecidableEq ι] {M : Type u_4} [CommMonoid M] (p : (ι → M) → Prop) (f : ι → M) (one : p 1) (mul : ∀ (f g : ι → M), p f → p g → p (HMul.hMul f g)) (mulSingle : ∀ (i : ι) (m : M), p (mulSingle i m)) : p f