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))
:
s.sum a = (Multiset.map (fun (f : (a : α) → β a) => f a) s).sum
theorem
Pi.multiset_prod_apply
{α : Type u_1}
{β : α → Type u_2}
[(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_1}
{β : α → Type u_2}
{γ : Type u_3}
[(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_1}
{β : α → Type u_2}
{γ : Type u_3}
[(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_1}
{β : α → Type u_2}
{γ : Type u_3}
[(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_1}
{β : α → Type u_2}
{γ : Type u_3}
[(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_1}
{β : α → Type u_2}
{γ : Type u_3}
[Fintype γ]
[(a : α) → AddCommMonoid (β a)]
(a : α)
(g : γ → (a : α) → β a)
:
(∑ c : γ, g c) a = ∑ 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)
:
(∏ c : γ, g c) a = ∏ c : γ, g c a
theorem
prod_mk_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[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_1}
{β : Type u_2}
{γ : Type u_3}
[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_1}
[Fintype ι]
[DecidableEq ι]
{R : Type u_2}
[Semiring R]
(x : ι → R)
:
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)
:
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)
:
∏ 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), 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
AddMonoidHom.functions_ext'_iff
{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}
:
g = h ↔ ∀ (i : I), g.comp (AddMonoidHom.single Z i) = h.comp (AddMonoidHom.single Z i)
theorem
MonoidHom.functions_ext'_iff
{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}
:
g = h ↔ ∀ (i : I), g.comp (MonoidHom.mulSingle Z i) = h.comp (MonoidHom.mulSingle Z i)
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), 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_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}
:
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 : γ → α × β}
:
(∑ c ∈ s, f c).1 = ∑ c ∈ s, (f c).1
theorem
Prod.fst_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[CommMonoid β]
{s : Finset γ}
{f : γ → α × β}
:
(∏ c ∈ s, f c).1 = ∏ c ∈ s, (f c).1
theorem
Prod.snd_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[AddCommMonoid α]
[AddCommMonoid β]
{s : Finset γ}
{f : γ → α × β}
:
(∑ c ∈ s, f c).2 = ∑ c ∈ s, (f c).2
theorem
Prod.snd_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[CommMonoid α]
[CommMonoid β]
{s : Finset γ}
{f : γ → α × β}
:
(∏ c ∈ s, f c).2 = ∏ c ∈ s, (f c).2