Big operators for Pi Types #
This file contains theorems relevant to big operators in binary and arbitrary product of monoids and groups
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 : I → Type 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 : I → Type 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 : I → Type 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 : I → Type 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 : I → Type 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 : I → Type 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 : I → Type 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