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_4} {β : α → Type u_5} [(a : α) → AddMonoid (β a)] (a : α) (l : List ((a : α) → β a)) : l.sum a = (List.map (fun (f : (a : α) → β a) => f a) l).sum

theorem Pi.list_prod_apply {α : Type u_4} {β : α → Type u_5} [(a : α) → Monoid (β a)] (a : α) (l : List ((a : α) → β a)) : l.prod a = (List.map (fun (f : (a : α) → β a) => f a) l).prod

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

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

@[simp]

theorem Finset.sum_apply {α : Type u_4} {β : α → Type u_5} {γ : Type u_6} [(a : α) → AddCommMonoid (β a)] (a : α) (s : Finset γ) (g : γ → (a : α) → β a) : (∑ c ∈ s, g c) a = ∑ c ∈ s, g c a

@[simp]

theorem Finset.prod_apply {α : Type u_4} {β : α → Type u_5} {γ : Type u_6} [(a : α) → CommMonoid (β a)] (a : α) (s : Finset γ) (g : γ → (a : α) → β a) : (∏ c ∈ s, g c) a = ∏ c ∈ s, g c a

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

An 'unapplied' analogue of Finset.sum_apply.

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

An 'unapplied' analogue of Finset.prod_apply.

theorem Fintype.sum_apply {α : Type u_4} {β : α → Type u_5} {γ : Type u_6} [Fintype γ] [(a : α) → AddCommMonoid (β a)] (a : α) (g : γ → (a : α) → β a) : (∑ c : γ, g c) a = ∑ c : γ, g c a

theorem Fintype.prod_apply {α : Type u_4} {β : α → Type u_5} {γ : Type u_6} [Fintype γ] [(a : α) → CommMonoid (β a)] (a : α) (g : γ → (a : α) → β a) : (∏ c : γ, g c) a = ∏ c : γ, g c a

theorem prod_mk_sum {α : Type u_4} {β : Type u_5} {γ : Type u_6} [AddCommMonoid α] [AddCommMonoid β] (s : Finset γ) (f : γ → α) (g : γ → β) : (∑ x ∈ s, f x, ∑ x ∈ s, g x) = ∑ x ∈ s, (f x, g x)

theorem prod_mk_prod {α : Type u_4} {β : Type u_5} {γ : Type u_6} [CommMonoid α] [CommMonoid β] (s : Finset γ) (f : γ → α) (g : γ → β) : (∏ x ∈ s, f x, ∏ x ∈ s, g x) = ∏ x ∈ s, (f x, g x)

theorem pi_eq_sum_univ {ι : Type u_4} [Fintype ι] [DecidableEq ι] {R : Type u_5} [Semiring R] (x : ι → R) : x = ∑ i : ι, x i • fun (j : ι) => if i = j then 1 else 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 : κ) : ∏ i ∈ s, (f i).indicator (g i) j = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) j

theorem prod_indicator {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [CommSemiring α] (s : Finset ι) (f : ι → Set κ) (g : ι → κ → α) : ∏ i ∈ s, (f i).indicator (g i) = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i)

theorem prod_indicator_const_apply {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [CommSemiring α] (s : Finset ι) (f : ι → Set κ) (g : κ → α) (j : κ) : ∏ i ∈ s, (f i).indicator g j = (⋂ x ∈ s, f x).indicator (g ^ s.card) j

theorem prod_indicator_const {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [CommSemiring α] (s : Finset ι) (f : ι → Set κ) (g : κ → α) : ∏ i ∈ s, (f i).indicator g = (⋂ x ∈ s, f x).indicator (g ^ s.card)

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

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) : ∏ i : I, Pi.mulSingle i (f i) = f

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 : ((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_4} [DecidableEq I] {Z : I → Type u_5} [(i : I) → CommMonoid (Z i)] [Finite I] (G : Type u_6) [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_4} [DecidableEq I] {Z : I → Type u_5} [(i : I) → AddCommMonoid (Z i)] [Finite I] (M : Type u_6) [AddCommMonoid M] (g : ((i : I) → Z i) →+ M) (h : ((i : I) → Z i) →+ M) (H : ∀ (i : I), g.comp (AddMonoidHom.single Z i) = h.comp (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'_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 : ((i : I) → Z i) →* M} {h : ((i : I) → Z i) →* M} : g = h ↔ ∀ (i : I), g.comp (MonoidHom.mulSingle Z i) = h.comp (MonoidHom.mulSingle Z i)

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 : ((i : I) → Z i) →+ M} {h : ((i : I) → Z i) →+ M} : g = h ↔ ∀ (i : I), g.comp (AddMonoidHom.single Z i) = h.comp (AddMonoidHom.single Z i)

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 : ((i : I) → Z i) →* M) (h : ((i : I) → Z i) →* M) (H : ∀ (i : I), g.comp (MonoidHom.mulSingle Z i) = h.comp (MonoidHom.mulSingle 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_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 : ((i : I) → f i) →+* G} {h : ((i : I) → f i) →+* G} : g = h ↔ ∀ (i : I) (x : f i), g (Pi.single i x) = h (Pi.single i x)

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 : ((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_4} {β : Type u_5} {γ : Type u_6} [AddCommMonoid α] [AddCommMonoid β] {s : Finset γ} {f : γ → α × β} : (∑ c ∈ s, f c).1 = ∑ c ∈ s, (f c).1

theorem Prod.fst_prod {α : Type u_4} {β : Type u_5} {γ : Type u_6} [CommMonoid α] [CommMonoid β] {s : Finset γ} {f : γ → α × β} : (∏ c ∈ s, f c).1 = ∏ c ∈ s, (f c).1

theorem Prod.snd_sum {α : Type u_4} {β : Type u_5} {γ : Type u_6} [AddCommMonoid α] [AddCommMonoid β] {s : Finset γ} {f : γ → α × β} : (∑ c ∈ s, f c).2 = ∑ c ∈ s, (f c).2

theorem Prod.snd_prod {α : Type u_4} {β : Type u_5} {γ : Type u_6} [CommMonoid α] [CommMonoid β] {s : Finset γ} {f : γ → α × β} : (∏ c ∈ s, f c).2 = ∏ c ∈ s, (f c).2