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 s a = Multiset.sum (Multiset.map (fun (f : (a : α) → β a) => f a) s)
theorem
Pi.multiset_prod_apply
{α : Type u_1}
{β : α → Type u_2}
[(a : α) → CommMonoid (β a)]
(a : α)
(s : Multiset ((a : α) → β a))
:
Multiset.prod s a = Multiset.prod (Multiset.map (fun (f : (a : α) → β a) => 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 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 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 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 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
pi_eq_sum_univ
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{R : Type u_2}
[Semiring R]
(x : ι → R)
:
x = Finset.sum Finset.univ fun (i : ι) => x i • fun (j : ι) => if i = j then 1 else 0
decomposing x : ι → R as a sum along the canonical basis
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 : 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 : 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.mulSingle Z i) = MonoidHom.comp h (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
{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).1 = Finset.sum s fun (c : γ) => (f c).1
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).1 = Finset.prod s fun (c : γ) => (f c).1
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).2 = Finset.sum s fun (c : γ) => (f c).2
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).2 = Finset.prod s fun (c : γ) => (f c).2