Big operators for Pi Types #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 : α), add_comm_monoid (β a)]
(a : α)
(s : multiset (Π (a : α), β a)) :
s.sum a = (multiset.map (λ (f : Π (a : α), β a), f a) s).sum
theorem
pi.multiset_prod_apply
{α : Type u_1}
{β : α → Type u_2}
[Π (a : α), comm_monoid (β a)]
(a : α)
(s : multiset (Π (a : α), β a)) :
s.prod a = (multiset.map (λ (f : Π (a : α), β a), f a) s).prod
theorem
finset.sum_fn
{α : Type u_1}
{β : α → Type u_2}
{γ : Type u_3}
[Π (a : α), add_comm_monoid (β a)]
(s : finset γ)
(g : γ → Π (a : α), β a) :
An 'unapplied' analogue of finset.sum_apply.
theorem
finset.prod_fn
{α : Type u_1}
{β : α → Type u_2}
{γ : Type u_3}
[Π (a : α), comm_monoid (β a)]
(s : finset γ)
(g : γ → Π (a : α), β a) :
An 'unapplied' analogue of finset.prod_apply.
@[simp]
theorem
fintype.sum_apply
{α : Type u_1}
{β : α → Type u_2}
{γ : Type u_3}
[fintype γ]
[Π (a : α), add_comm_monoid (β a)]
(a : α)
(g : γ → Π (a : α), β a) :
finset.univ.sum (λ (c : γ), g c) a = finset.univ.sum (λ (c : γ), g c a)
@[simp]
theorem
fintype.prod_apply
{α : Type u_1}
{β : α → Type u_2}
{γ : Type u_3}
[fintype γ]
[Π (a : α), comm_monoid (β a)]
(a : α)
(g : γ → Π (a : α), β a) :
finset.univ.prod (λ (c : γ), g c) a = finset.univ.prod (λ (c : γ), g c a)
theorem
prod_mk_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[comm_monoid α]
[comm_monoid β]
(s : finset γ)
(f : γ → α)
(g : γ → β) :
theorem
prod_mk_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[add_comm_monoid β]
(s : finset γ)
(f : γ → α)
(g : γ → β) :
theorem
finset.univ_sum_single
{I : Type u_1}
[decidable_eq I]
{Z : I → Type u_2}
[Π (i : I), add_comm_monoid (Z i)]
[fintype I]
(f : Π (i : I), Z i) :
finset.univ.sum (λ (i : I), pi.single i (f i)) = f
theorem
finset.univ_prod_mul_single
{I : Type u_1}
[decidable_eq I]
{Z : I → Type u_2}
[Π (i : I), comm_monoid (Z i)]
[fintype I]
(f : Π (i : I), Z i) :
finset.univ.prod (λ (i : I), pi.mul_single i (f i)) = f
theorem
monoid_hom.functions_ext
{I : Type u_1}
[decidable_eq I]
{Z : I → Type u_2}
[Π (i : I), comm_monoid (Z i)]
[finite I]
(G : Type u_3)
[comm_monoid G]
(g h : (Π (i : I), Z i) →* G)
(H : ∀ (i : I) (x : Z i), ⇑g (pi.mul_single i x) = ⇑h (pi.mul_single i x)) :
g = h
theorem
add_monoid_hom.functions_ext
{I : Type u_1}
[decidable_eq I]
{Z : I → Type u_2}
[Π (i : I), add_comm_monoid (Z i)]
[finite I]
(G : Type u_3)
[add_comm_monoid G]
(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
@[ext]
theorem
add_monoid_hom.functions_ext'
{I : Type u_1}
[decidable_eq I]
{Z : I → Type u_2}
[Π (i : I), add_comm_monoid (Z i)]
[finite I]
(M : Type u_3)
[add_comm_monoid M]
(g h : (Π (i : I), Z i) →+ M)
(H : ∀ (i : I), g.comp (add_monoid_hom.single Z i) = h.comp (add_monoid_hom.single Z i)) :
g = h
This is used as the ext lemma instead of add_monoid_hom.functions_ext for reasons explained in
note [partially-applied ext lemmas].
@[ext]
theorem
monoid_hom.functions_ext'
{I : Type u_1}
[decidable_eq I]
{Z : I → Type u_2}
[Π (i : I), comm_monoid (Z i)]
[finite I]
(M : Type u_3)
[comm_monoid M]
(g h : (Π (i : I), Z i) →* M)
(H : ∀ (i : I), g.comp (monoid_hom.single Z i) = h.comp (monoid_hom.single Z i)) :
g = h
This is used as the ext lemma instead of monoid_hom.functions_ext for reasons explained in
note [partially-applied ext lemmas].
@[ext]
theorem
ring_hom.functions_ext
{I : Type u_1}
[decidable_eq I]
{f : I → Type u_2}
[Π (i : I), non_assoc_semiring (f i)]
[finite I]
(G : Type u_3)
[non_assoc_semiring G]
(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_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[comm_monoid α]
[comm_monoid β]
{s : finset γ}
{f : γ → α × β} :
theorem
prod.fst_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[add_comm_monoid β]
{s : finset γ}
{f : γ → α × β} :
theorem
prod.snd_prod
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[comm_monoid α]
[comm_monoid β]
{s : finset γ}
{f : γ → α × β} :
theorem
prod.snd_sum
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[add_comm_monoid α]
[add_comm_monoid β]
{s : finset γ}
{f : γ → α × β} :