Documentation

Mathlib.Algebra.BigOperators.Pi

Big operators for Pi Types #

This file contains theorems relevant to big operators in binary and arbitrary products of monoids and groups.

source
theorem Pi.list_prod_apply {α : Type u_7} {M : α → Type u_8} [(a : α) → Monoid (M a)] (a : α) (l : List ((a : α) → M a)) :
l.prod a = (List.map (fun (f : (a : α) → M a) => f a) l).prod
source
theorem Pi.list_sum_apply {α : Type u_7} {M : α → Type u_8} [(a : α) → AddMonoid (M a)] (a : α) (l : List ((a : α) → M a)) :
l.sum a = (List.map (fun (f : (a : α) → M a) => f a) l).sum
source
theorem Pi.multiset_prod_apply {α : Type u_7} {M : α → Type u_8} [(a : α) → CommMonoid (M a)] (a : α) (s : Multiset ((a : α) → M a)) :
s.prod a = (Multiset.map (fun (f : (a : α) → M a) => f a) s).prod
source
theorem Pi.multiset_sum_apply {α : Type u_7} {M : α → Type u_8} [(a : α) → AddCommMonoid (M a)] (a : α) (s : Multiset ((a : α) → M a)) :
s.sum a = (Multiset.map (fun (f : (a : α) → M a) => f a) s).sum
source
@[simp]
theorem Finset.prod_apply {ι : Type u_1} {α : Type u_7} {M : α → Type u_8} [(a : α) → CommMonoid (M a)] (a : α) (s : Finset ι) (g : ι → (a : α) → M a) :
(∏ c ∈ s, g c) a = ∏ c ∈ s, g c a
source
@[simp]
theorem Finset.sum_apply {ι : Type u_1} {α : Type u_7} {M : α → Type u_8} [(a : α) → AddCommMonoid (M a)] (a : α) (s : Finset ι) (g : ι → (a : α) → M a) :
(∑ c ∈ s, g c) a = ∑ c ∈ s, g c a
source
theorem Finset.prod_fn {α : Type u_7} {M : α → Type u_8} {ι : Type u_9} [(a : α) → CommMonoid (M a)] (s : Finset ι) (g : ι → (a : α) → M a) :
∏ c ∈ s, g c = fun (a : α) => ∏ c ∈ s, g c a

An 'unapplied' analogue of Finset.prod_apply.

source
theorem Finset.sum_fn {α : Type u_7} {M : α → Type u_8} {ι : Type u_9} [(a : α) → AddCommMonoid (M a)] (s : Finset ι) (g : ι → (a : α) → M a) :
∑ c ∈ s, g c = fun (a : α) => ∑ c ∈ s, g c a

An 'unapplied' analogue of Finset.sum_apply.

source
theorem Fintype.prod_apply {ι : Type u_1} {α : Type u_7} {M : α → Type u_8} [Fintype ι] [(a : α) → CommMonoid (M a)] (a : α) (g : ι → (a : α) → M a) :
(∏ c : ι, g c) a = ∏ c : ι, g c a
source
theorem Fintype.sum_apply {ι : Type u_1} {α : Type u_7} {M : α → Type u_8} [Fintype ι] [(a : α) → AddCommMonoid (M a)] (a : α) (g : ι → (a : α) → M a) :
(∑ c : ι, g c) a = ∑ c : ι, g c a
source
theorem prod_mk_prod {ι : Type u_1} {M : Type u_3} {N : Type u_4} [CommMonoid M] [CommMonoid N] (s : Finset ι) (f : ι → M) (g : ι → N) :
(∏ x ∈ s, f x, ∏ x ∈ s, g x) = ∏ x ∈ s, (f x, g x)
source
theorem prod_mk_sum {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] (s : Finset ι) (f : ι → M) (g : ι → N) :
(∑ x ∈ s, f x, ∑ x ∈ s, g x) = ∑ x ∈ s, (f x, g x)
source
theorem pi_eq_sum_univ {ι : Type u_7} [Fintype ι] [DecidableEq ι] {R : Type u_8} [NonAssocSemiring 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

source
theorem pi_eq_sum_univ' {ι : Type u_7} [Fintype ι] [DecidableEq ι] {R : Type u_8} [NonAssocSemiring R] (x : ι → R) :
x = ∑ i : ι, x i • Pi.single i 1

Decomposing x : ι → R as a sum along the canonical basis Pi.single i 1 for i : ι.

source
theorem prod_indicator_apply {ι : Type u_1} {κ : Type u_2} {R : Type u_5} [CommSemiring R] (s : Finset ι) (f : ι → Set κ) (g : ι → κ → R) (j : κ) :
∏ i ∈ s, (f i).indicator (g i) j = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i) j
source
theorem prod_indicator {ι : Type u_1} {κ : Type u_2} {R : Type u_5} [CommSemiring R] (s : Finset ι) (f : ι → Set κ) (g : ι → κ → R) :
∏ i ∈ s, (f i).indicator (g i) = (⋂ x ∈ s, f x).indicator (∏ i ∈ s, g i)
source
theorem prod_indicator_const_apply {ι : Type u_1} {κ : Type u_2} {R : Type u_5} [CommSemiring R] (s : Finset ι) (f : ι → Set κ) (g : κ → R) (j : κ) :
∏ i ∈ s, (f i).indicator g j = (⋂ x ∈ s, f x).indicator (g ^ s.card) j
source
theorem prod_indicator_const {ι : Type u_1} {κ : Type u_2} {R : Type u_5} [CommSemiring R] (s : Finset ι) (f : ι → Set κ) (g : κ → R) :
∏ i ∈ s, (f i).indicator g = (⋂ x ∈ s, f x).indicator (g ^ s.card)
source
theorem Finset.univ_prod_mulSingle {I : Type u_7} [DecidableEq I] {M : I → Type u_8} [(i : I) → CommMonoid (M i)] [Fintype I] (f : (i : I) → M i) :
∏ i : I, Pi.mulSingle i (f i) = f
source
theorem Finset.univ_sum_single {I : Type u_7} [DecidableEq I] {M : I → Type u_8} [(i : I) → AddCommMonoid (M i)] [Fintype I] (f : (i : I) → M i) :
∑ i : I, Pi.single i (f i) = f
source
theorem MonoidHom.functions_ext {I : Type u_7} [DecidableEq I] {M : I → Type u_8} [(i : I) → CommMonoid (M i)] [Finite I] (N : Type u_9) [CommMonoid N] (g h : ((i : I) → M i) →* N) (H : ∀ (i : I) (x : M i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)) :
g = h
source
theorem AddMonoidHom.functions_ext {I : Type u_7} [DecidableEq I] {M : I → Type u_8} [(i : I) → AddCommMonoid (M i)] [Finite I] (N : Type u_9) [AddCommMonoid N] (g h : ((i : I) → M i) →+ N) (H : ∀ (i : I) (x : M i), g (Pi.single i x) = h (Pi.single i x)) :
g = h
source
theorem MonoidHom.functions_ext' {I : Type u_7} [DecidableEq I] {M : I → Type u_8} [(i : I) → CommMonoid (M i)] [Finite I] (N : Type u_9) [CommMonoid N] (g h : ((i : I) → M i) →* N) (H : ∀ (i : I), g.comp (mulSingle M i) = h.comp (mulSingle M i)) :
g = h

This is used as the ext lemma instead of MonoidHom.functions_ext for reasons explained in note [partially-applied ext lemmas].

source
theorem AddMonoidHom.functions_ext' {I : Type u_7} [DecidableEq I] {M : I → Type u_8} [(i : I) → AddCommMonoid (M i)] [Finite I] (N : Type u_9) [AddCommMonoid N] (g h : ((i : I) → M i) →+ N) (H : ∀ (i : I), g.comp (single M i) = h.comp (single M i)) :
g = h

This is used as the ext lemma instead of AddMonoidHom.functions_ext for reasons explained in note [partially-applied ext lemmas].

source
theorem AddMonoidHom.functions_ext'_iff {I : Type u_7} [DecidableEq I] {M : I → Type u_8} [(i : I) → AddCommMonoid (M i)] [Finite I] {N : Type u_9} [AddCommMonoid N] {g h : ((i : I) → M i) →+ N} :
g = h ↔ ∀ (i : I), g.comp (single M i) = h.comp (single M i)
source
theorem MonoidHom.functions_ext'_iff {I : Type u_7} [DecidableEq I] {M : I → Type u_8} [(i : I) → CommMonoid (M i)] [Finite I] {N : Type u_9} [CommMonoid N] {g h : ((i : I) → M i) →* N} :
g = h ↔ ∀ (i : I), g.comp (mulSingle M i) = h.comp (mulSingle M i)
source
theorem RingHom.functions_ext {I : Type u_7} [DecidableEq I] {R : I → Type u_8} [(i : I) → NonAssocSemiring (R i)] [Finite I] (S : Type u_9) [NonAssocSemiring S] (g h : ((i : I) → R i) →+* S) (H : ∀ (i : I) (x : R i), g (Pi.single i x) = h (Pi.single i x)) :
g = h
source
theorem RingHom.functions_ext_iff {I : Type u_7} [DecidableEq I] {R : I → Type u_8} [(i : I) → NonAssocSemiring (R i)] [Finite I] {S : Type u_9} [NonAssocSemiring S] {g h : ((i : I) → R i) →+* S} :
g = h ↔ ∀ (i : I) (x : R i), g (Pi.single i x) = h (Pi.single i x)
source
theorem Prod.fst_prod {ι : Type u_1} {M : Type u_3} {N : Type u_4} [CommMonoid M] [CommMonoid N] {s : Finset ι} {f : ι → M × N} :
(∏ c ∈ s, f c).1 = ∏ c ∈ s, (f c).1
source
theorem Prod.fst_sum {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] {s : Finset ι} {f : ι → M × N} :
(∑ c ∈ s, f c).1 = ∑ c ∈ s, (f c).1
source
theorem Prod.snd_prod {ι : Type u_1} {M : Type u_3} {N : Type u_4} [CommMonoid M] [CommMonoid N] {s : Finset ι} {f : ι → M × N} :
(∏ c ∈ s, f c).2 = ∏ c ∈ s, (f c).2
source
theorem Prod.snd_sum {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] {s : Finset ι} {f : ι → M × N} :
(∑ c ∈ s, f c).2 = ∑ c ∈ s, (f c).2
source
def Pi.monoidHomMulEquiv {ι : Type u_7} [Fintype ι] [DecidableEq ι] (M : ι → Type u_8) [(i : ι) → CommMonoid (M i)] (M' : Type u_9) [CommMonoid M'] :
(((i : ι) → M i) →* M') ≃* ((i : ι) → M i →* M')

The canonical isomorphism between the monoid of homomorphisms from a finite product of commutative monoids to another commutative monoid and the product of the homomorphism monoids.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Pi.addMonoidHomAddEquiv {ι : Type u_7} [Fintype ι] [DecidableEq ι] (M : ι → Type u_8) [(i : ι) → AddCommMonoid (M i)] (M' : Type u_9) [AddCommMonoid M'] :
    (((i : ι) → M i) →+ M') ≃+ ((i : ι) → M i →+ M')

    The canonical isomorphism between the additive monoid of homomorphisms from a finite product of additive commutative monoids to another additive commutative monoid and the product of the homomorphism monoids.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Pi.single_induction {ι : Type u_1} [Finite ι] [DecidableEq ι] {M : ι → Type u_7} [(i : ι) → AddCommMonoid (M i)] (p : ((i : ι) → M i) → Prop) (f : (i : ι) → M i) (zero : p 0) (add : ∀ (f g : (i : ι) → M i), p f → p g → p (f + g)) (single : ∀ (i : ι) (m : M i), p (single i m)) :
      p f
      source
      theorem Pi.mulSingle_induction {ι : Type u_1} [Finite ι] [DecidableEq ι] {M : ι → Type u_7} [(i : ι) → CommMonoid (M i)] (p : ((i : ι) → M i) → Prop) (f : (i : ι) → M i) (one : p 1) (mul : ∀ (f g : (i : ι) → M i), p f → p g → p (f * g)) (mulSingle : ∀ (i : ι) (m : M i), p (mulSingle i m)) :
      p f
      source
      theorem eqOn_finsetProd {ι : Type u_8} {α : Type u_9} {β : Type u_10} [CommMonoid α] {s : Set β} {f f' : ι → β → α} (h : ∀ (i : ι), Set.EqOn (f i) (f' i) s) (v : Finset ι) :
      Set.EqOn (∏ i ∈ v, f i) (∏ i ∈ v, f' i) s
      source
      theorem eqOn_finsetSum {ι : Type u_8} {α : Type u_9} {β : Type u_10} [AddCommMonoid α] {s : Set β} {f f' : ι → β → α} (h : ∀ (i : ι), Set.EqOn (f i) (f' i) s) (v : Finset ι) :
      Set.EqOn (∑ i ∈ v, f i) (∑ i ∈ v, f' i) s
      source
      theorem eqOn_fun_finsetProd {ι : Type u_8} {α : Type u_9} {β : Type u_10} [CommMonoid α] {s : Set β} {f f' : ι → β → α} (h : ∀ (i : ι), Set.EqOn (f i) (f' i) s) (v : Finset ι) :
      Set.EqOn (fun (b : β) => ∏ i ∈ v, f i b) (fun (b : β) => ∏ i ∈ v, f' i b) s
      source
      theorem eqOn_fun_finsetSum {ι : Type u_8} {α : Type u_9} {β : Type u_10} [AddCommMonoid α] {s : Set β} {f f' : ι → β → α} (h : ∀ (i : ι), Set.EqOn (f i) (f' i) s) (v : Finset ι) :
      Set.EqOn (fun (b : β) => ∑ i ∈ v, f i b) (fun (b : β) => ∑ i ∈ v, f' i b) s