Big operators

In this file we define products and sums indexed by finite sets (specifically, Finset).

Notation

We introduce the following notation.

Let s be a Finset ι, and f : ι → β a function.

• ∏ x ∈ s, f x is notation for Finset.prod s f (assuming β is a CommMonoid)
• ∑ x ∈ s, f x is notation for Finset.sum s f (assuming β is an AddCommMonoid)
• ∏ x, f x is notation for Finset.prod Finset.univ f (assuming ι is a Fintype and β is a CommMonoid)
• ∑ x, f x is notation for Finset.sum Finset.univ f (assuming ι is a Fintype and β is an AddCommMonoid)
• ∏ x ∈ s with p x, f x is notation for Finset.prod (Finset.filter p s) f.
• ∑ x ∈ s with p x, f x is notation for Finset.sum (Finset.filter p s) f.
• ∏ (x ∈ s) (y ∈ t), f x y is notation for Finset.prod (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y).
• ∑ (x ∈ s) (y ∈ t), f x y is notation for Finset.sum (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y).
• Other supported binders: x < n, x > n, x ≤ n, x ≥ n, x ≠ n, x ∉ s, x + y = n

Implementation Notes

The first arguments in all definitions and lemmas is the codomain of the function of the big operator. This is necessary for the heuristic in @[to_additive]. See the documentation of to_additive.attr for more information.

def Finset.prod {ι : Type u_1} {M : Type u_3} [CommMonoid M] (s : Finset ι) (f : ι → M) : M

∏ x ∈ s, f x is the product of f x as x ranges over the elements of the finite set s.

When the index type is a Fintype, the notation ∏ x, f x, is a shorthand for ∏ x ∈ Finset.univ, f x.

def Finset.sum {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : M

∑ x ∈ s, f x is the sum of f x as x ranges over the elements of the finite set s.

When the index type is a Fintype, the notation ∑ x, f x, is a shorthand for ∑ x ∈ Finset.univ, f x.

@[simp]

theorem Finset.prod_mk {ι : Type u_1} {M : Type u_3} [CommMonoid M] (s : Multiset ι) (hs : s.Nodup) (f : ι → M) : { val := s, nodup := hs }.prod f = (Multiset.map f s).prod

@[simp]

theorem Finset.sum_mk {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Multiset ι) (hs : s.Nodup) (f : ι → M) : { val := s, nodup := hs }.sum f = (Multiset.map f s).sum

@[simp]

theorem Finset.prod_val {M : Type u_3} [CommMonoid M] (s : Finset M) : s.val.prod = s.prod id

@[simp]

theorem Finset.sum_val {M : Type u_3} [AddCommMonoid M] (s : Finset M) : s.val.sum = s.sum id

def LibraryNote.operator_precedence_of_big_operators : Batteries.Util.LibraryNote

There is no established mathematical convention for the operator precedence of big operators like ∏ and ∑. We will have to make a choice.

Online discussions, such as https://math.stackexchange.com/q/185538/30839 seem to suggest that ∏ and ∑ should have the same precedence, and that this should be somewhere between * and +. The latter have precedence levels 70 and 65 respectively, and we therefore choose the level 67.

In practice, this means that parentheses should be placed as follows:

∑ k ∈ K, (a k + b k) = ∑ k ∈ K, a k + ∑ k ∈ K, b k →
  ∏ k ∈ K, a k * b k = (∏ k ∈ K, a k) * (∏ k ∈ K, b k)

(Example taken from page 490 of Knuth's Concrete Mathematics.)

def BigOperators.bigOpBinder : Lean.ParserDescr

A bigOpBinder is like an extBinder and has the form x, x : ty, or x pred where pred is a binderPred like < 2. Unlike extBinder, x is a term.

def BigOperators.bigOpBinderParenthesized : Lean.ParserDescr

A BigOperator binder in parentheses

def BigOperators.bigOpBinderCollection : Lean.ParserDescr

A list of parenthesized binders

def BigOperators.bigOpBinders : Lean.ParserDescr

A single (unparenthesized) binder, or a list of parenthesized binders

def BigOperators.processBigOpBinder (processed : Array (Lean.Term × Lean.Term)) (binder : Lean.TSyntax `BigOperators.bigOpBinder) : Lean.MacroM (Array (Lean.Term × Lean.Term))

Collects additional binder/Finset pairs for the given bigOpBinder.

Note: this is not extensible at the moment, unlike the usual bigOpBinder expansions.

def BigOperators.processBigOpBinders (binders : Lean.TSyntax `BigOperators.bigOpBinders) : Lean.MacroM (Array (Lean.Term × Lean.Term))

Collects the binder/Finset pairs for the given bigOpBinders.

def BigOperators.bigOpBindersPattern (processed : Array (Lean.Term × Lean.Term)) : Lean.MacroM Lean.Term

Collects the binderIdents into a ⟨...⟩ expression.

def BigOperators.bigOpBindersProd (processed : Array (Lean.Term × Lean.Term)) : Lean.MacroM Lean.Term

Collects the terms into a product of sets.

def BigOperators.bigsum : Lean.ParserDescr

• ∑ x, f x is notation for Finset.sum Finset.univ f. It is the sum of f x, where x ranges over the finite domain of f.
• ∑ x ∈ s, f x is notation for Finset.sum s f. It is the sum of f x, where x ranges over the finite set s (either a Finset or a Set with a Fintype instance).
• ∑ x ∈ s with p x, f x is notation for Finset.sum (Finset.filter p s) f.
• ∑ x ∈ s with h : p x, f x h is notation for Finset.sum s fun x ↦ if h : p x then f x h else 0.
• ∑ (x ∈ s) (y ∈ t), f x y is notation for Finset.sum (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y).

These support destructuring, for example ∑ ⟨x, y⟩ ∈ s ×ˢ t, f x y.

Notation: "∑" bigOpBinders* (" with" (ident ":")? term)? "," term

def BigOperators.bigprod : Lean.ParserDescr

• ∏ x, f x is notation for Finset.prod Finset.univ f. It is the product of f x, where x ranges over the finite domain of f.
• ∏ x ∈ s, f x is notation for Finset.prod s f. It is the product of f x, where x ranges over the finite set s (either a Finset or a Set with a Fintype instance).
• ∏ x ∈ s with p x, f x is notation for Finset.prod (Finset.filter p s) f.
• ∏ x ∈ s with h : p x, f x h is notation for Finset.prod s fun x ↦ if h : p x then f x h else 1.
• ∏ (x ∈ s) (y ∈ t), f x y is notation for Finset.prod (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y).

These support destructuring, for example ∏ ⟨x, y⟩ ∈ s ×ˢ t, f x y.

Notation: "∏" bigOpBinders* ("with" (ident ":")? term)? "," term

def BigOperators.delabFinsetProd : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for Finset.prod. The pp.funBinderTypes option controls whether to show the domain type when the product is over Finset.univ.

def BigOperators.delabFinsetSum : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for Finset.sum. The pp.funBinderTypes option controls whether to show the domain type when the sum is over Finset.univ.

theorem Finset.prod_eq_multiset_prod {ι : Type u_1} {M : Type u_3} [CommMonoid M] (s : Finset ι) (f : ι → M) : ∏ x ∈ s, f x = (Multiset.map f s.val).prod

theorem Finset.sum_eq_multiset_sum {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : ∑ x ∈ s, f x = (Multiset.map f s.val).sum

@[simp]

theorem Finset.prod_map_val {ι : Type u_1} {M : Type u_3} [CommMonoid M] (s : Finset ι) (f : ι → M) : (Multiset.map f s.val).prod = ∏ a ∈ s, f a

@[simp]

theorem Finset.sum_map_val {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : (Multiset.map f s.val).sum = ∑ a ∈ s, f a

@[simp]

theorem Finset.sum_multiset_singleton {ι : Type u_1} (s : Finset ι) : ∑ a ∈ s, {a} = s.val

@[simp]

theorem map_prod {ι : Type u_1} {M : Type u_3} {N : Type u_4} [CommMonoid M] [CommMonoid N] {G : Type u_7} [FunLike G M N] [MonoidHomClass G M N] (g : G) (f : ι → M) (s : Finset ι) : g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)

@[simp]

theorem map_sum {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] {G : Type u_7} [FunLike G M N] [AddMonoidHomClass G M N] (g : G) (f : ι → M) (s : Finset ι) : g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x)

@[simp]

theorem Finset.prod_empty {ι : Type u_1} {M : Type u_3} {f : ι → M} [CommMonoid M] : ∏ x ∈ ∅, f x = 1

@[simp]

theorem Finset.sum_empty {ι : Type u_1} {M : Type u_3} {f : ι → M} [AddCommMonoid M] : ∑ x ∈ ∅, f x = 0

theorem Finset.prod_empty' {ι : Type u_1} {M : Type u_3} [CommMonoid M] : ∅.prod = fun (x : ι → M) => 1

Variant of prod_empty not applied to a function.

theorem Finset.sum_empty' {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] : ∅.sum = fun (x : ι → M) => 0

theorem Finset.prod_of_isEmpty {ι : Type u_1} {M : Type u_3} {f : ι → M} [CommMonoid M] [IsEmpty ι] (s : Finset ι) : ∏ i ∈ s, f i = 1

theorem Finset.sum_of_isEmpty {ι : Type u_1} {M : Type u_3} {f : ι → M} [AddCommMonoid M] [IsEmpty ι] (s : Finset ι) : ∑ i ∈ s, f i = 0

@[simp]

theorem Finset.prod_const_one {ι : Type u_1} {M : Type u_3} {s : Finset ι} [CommMonoid M] : ∏ _x ∈ s, 1 = 1

@[simp]

theorem Finset.sum_const_zero {ι : Type u_1} {M : Type u_3} {s : Finset ι} [AddCommMonoid M] : ∑ _x ∈ s, 0 = 0

@[simp]

theorem Finset.prod_map {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [CommMonoid M] (s : Finset ι) (e : ι ↪ κ) (f : κ → M) : ∏ x ∈ map e s, f x = ∏ x ∈ s, f (e x)

@[simp]

theorem Finset.sum_map {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (e : ι ↪ κ) (f : κ → M) : ∑ x ∈ map e s, f x = ∑ x ∈ s, f (e x)

theorem Finset.prod_map' {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [CommMonoid M] (s : Finset ι) (e : ι ↪ κ) : (map e s).prod = fun (f : κ → M) => ∏ x ∈ s, f (e x)

Variant of prod_map not applied to a function.

theorem Finset.sum_map' {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (e : ι ↪ κ) : (map e s).sum = fun (f : κ → M) => ∑ x ∈ s, f (e x)

@[simp]

theorem Finset.prod_map_toList {ι : Type u_1} {M : Type u_3} [CommMonoid M] (s : Finset ι) (f : ι → M) : (List.map f s.toList).prod = s.prod f

@[simp]

theorem Finset.sum_map_toList {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : (List.map f s.toList).sum = s.sum f

@[simp]

theorem Finset.prod_toList {M : Type u_7} [CommMonoid M] (s : Finset M) : s.toList.prod = ∏ x ∈ s, x

@[simp]

theorem Finset.sum_toList {M : Type u_7} [AddCommMonoid M] (s : Finset M) : s.toList.sum = ∑ x ∈ s, x

theorem Equiv.Perm.prod_comp {ι : Type u_1} {M : Type u_3} [CommMonoid M] (σ : Perm ι) (s : Finset ι) (f : ι → M) (hs : {a : ι | σ a ≠ a} ⊆ ↑s) : ∏ x ∈ s, f (σ x) = ∏ x ∈ s, f x

theorem Equiv.Perm.sum_comp {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (σ : Perm ι) (s : Finset ι) (f : ι → M) (hs : {a : ι | σ a ≠ a} ⊆ ↑s) : ∑ x ∈ s, f (σ x) = ∑ x ∈ s, f x

theorem Equiv.Perm.prod_comp' {ι : Type u_1} {M : Type u_3} [CommMonoid M] (σ : Perm ι) (s : Finset ι) (f : ι → ι → M) (hs : {a : ι | σ a ≠ a} ⊆ ↑s) : ∏ x ∈ s, f (σ x) x = ∏ x ∈ s, f x ((Equiv.symm σ) x)

theorem Equiv.Perm.sum_comp' {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (σ : Perm ι) (s : Finset ι) (f : ι → ι → M) (hs : {a : ι | σ a ≠ a} ⊆ ↑s) : ∑ x ∈ s, f (σ x) x = ∑ x ∈ s, f x ((Equiv.symm σ) x)

theorem Finset.prod_bij {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (i : (a : ι) → a ∈ s → κ) (hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t) (i_inj : ∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, ∃ (a : ι) (ha : a ∈ s), i a ha = b) (h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) : ∏ x ∈ s, f x = ∏ x ∈ t, g x

Reorder a product.

The difference with Finset.prod_bij' is that the bijection is specified as a surjective injection, rather than by an inverse function.

The difference with Finset.prod_nbij is that the bijection is allowed to use membership of the domain of the product, rather than being a non-dependent function.

theorem Finset.sum_bij {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (i : (a : ι) → a ∈ s → κ) (hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t) (i_inj : ∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, ∃ (a : ι) (ha : a ∈ s), i a ha = b) (h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) : ∑ x ∈ s, f x = ∑ x ∈ t, g x

Reorder a sum.

The difference with Finset.sum_bij' is that the bijection is specified as a surjective injection, rather than by an inverse function.

The difference with Finset.sum_nbij is that the bijection is allowed to use membership of the domain of the sum, rather than being a non-dependent function.

theorem Finset.prod_bij' {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (i : (a : ι) → a ∈ s → κ) (j : (a : κ) → a ∈ t → ι) (hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t) (hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s) (left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a) (right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a) (h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) : ∏ x ∈ s, f x = ∏ x ∈ t, g x

Reorder a product.

The difference with Finset.prod_bij is that the bijection is specified with an inverse, rather than as a surjective injection.

The difference with Finset.prod_nbij' is that the bijection and its inverse are allowed to use membership of the domains of the products, rather than being non-dependent functions.

theorem Finset.sum_bij' {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (i : (a : ι) → a ∈ s → κ) (j : (a : κ) → a ∈ t → ι) (hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t) (hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s) (left_neg : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a) (right_neg : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a) (h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)) : ∑ x ∈ s, f x = ∑ x ∈ t, g x

Reorder a sum.

The difference with Finset.sum_bij is that the bijection is specified with an inverse, rather than as a surjective injection.

The difference with Finset.sum_nbij' is that the bijection and its inverse are allowed to use membership of the domains of the sums, rather than being non-dependent functions.

theorem Finset.prod_nbij {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (i_inj : Set.InjOn i ↑s) (i_surj : Set.SurjOn i ↑s ↑t) (h : ∀ a ∈ s, f a = g (i a)) : ∏ x ∈ s, f x = ∏ x ∈ t, g x

Reorder a product.

The difference with Finset.prod_nbij' is that the bijection is specified as a surjective injection, rather than by an inverse function.

The difference with Finset.prod_bij is that the bijection is a non-dependent function, rather than being allowed to use membership of the domain of the product.

theorem Finset.sum_nbij {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (i_inj : Set.InjOn i ↑s) (i_surj : Set.SurjOn i ↑s ↑t) (h : ∀ a ∈ s, f a = g (i a)) : ∑ x ∈ s, f x = ∑ x ∈ t, g x

Reorder a sum.

The difference with Finset.sum_nbij' is that the bijection is specified as a surjective injection, rather than by an inverse function.

The difference with Finset.sum_bij is that the bijection is a non-dependent function, rather than being allowed to use membership of the domain of the sum.

theorem Finset.prod_nbij' {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (i : ι → κ) (j : κ → ι) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s) (left_inv : ∀ a ∈ s, j (i a) = a) (right_inv : ∀ a ∈ t, i (j a) = a) (h : ∀ a ∈ s, f a = g (i a)) : ∏ x ∈ s, f x = ∏ x ∈ t, g x

Reorder a product.

The difference with Finset.prod_nbij is that the bijection is specified with an inverse, rather than as a surjective injection.

The difference with Finset.prod_bij' is that the bijection and its inverse are non-dependent functions, rather than being allowed to use membership of the domains of the products.

The difference with Finset.prod_equiv is that bijectivity is only required to hold on the domains of the products, rather than on the entire types.

theorem Finset.sum_nbij' {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (i : ι → κ) (j : κ → ι) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s) (left_neg : ∀ a ∈ s, j (i a) = a) (right_neg : ∀ a ∈ t, i (j a) = a) (h : ∀ a ∈ s, f a = g (i a)) : ∑ x ∈ s, f x = ∑ x ∈ t, g x

Reorder a sum.

The difference with Finset.sum_nbij is that the bijection is specified with an inverse, rather than as a surjective injection.

The difference with Finset.sum_bij' is that the bijection and its inverse are non-dependent functions, rather than being allowed to use membership of the domains of the sums.

The difference with Finset.sum_equiv is that bijectivity is only required to hold on the domains of the sums, rather than on the entire types.

theorem Finset.prod_equiv {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (e : ι ≃ κ) (hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) : ∏ i ∈ s, f i = ∏ i ∈ t, g i

Specialization of Finset.prod_nbij' that automatically fills in most arguments.

See Fintype.prod_equiv for the version where s and t are univ.

theorem Finset.sum_equiv {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (e : ι ≃ κ) (hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) : ∑ i ∈ s, f i = ∑ i ∈ t, g i

Specialization of Finset.sum_nbij' that automatically fills in most arguments.

See Fintype.sum_equiv for the version where s and t are univ.

theorem Finset.prod_bijective {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (e : ι → κ) (he : Function.Bijective e) (hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) : ∏ i ∈ s, f i = ∏ i ∈ t, g i

Specialization of Finset.prod_bij that automatically fills in most arguments.

See Fintype.prod_bijective for the version where s and t are univ.

theorem Finset.sum_bijective {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (e : ι → κ) (he : Function.Bijective e) (hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) : ∑ i ∈ s, f i = ∑ i ∈ t, g i

Specialization of Finset.sum_bij that automatically fills in most arguments.

See Fintype.sum_bijective for the version where s and t are univ.

theorem Finset.prod_hom_rel {ι : Type u_1} {M : Type u_3} {N : Type u_4} [CommMonoid M] [CommMonoid N] {r : M → N → Prop} {f : ι → M} {g : ι → N} {s : Finset ι} (h₁ : r 1 1) (h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)) : r (∏ x ∈ s, f x) (∏ x ∈ s, g x)

theorem Finset.sum_hom_rel {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] {r : M → N → Prop} {f : ι → M} {g : ι → N} {s : Finset ι} (h₁ : r 0 0) (h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a + b) (g a + c)) : r (∑ x ∈ s, f x) (∑ x ∈ s, g x)

theorem Finset.prod_coe_sort_eq_attach {ι : Type u_1} {M : Type u_3} (s : Finset ι) [CommMonoid M] (f : ↥s → M) : ∏ i : ↥s, f i = ∏ i ∈ s.attach, f i

theorem Finset.sum_coe_sort_eq_attach {ι : Type u_1} {M : Type u_3} (s : Finset ι) [AddCommMonoid M] (f : ↥s → M) : ∑ i : ↥s, f i = ∑ i ∈ s.attach, f i

theorem Finset.prod_ite_index {ι : Type u_1} {M : Type u_3} [CommMonoid M] (p : Prop) [Decidable p] (s t : Finset ι) (f : ι → M) : ∏ x ∈ if p then s else t, f x = if p then ∏ x ∈ s, f x else ∏ x ∈ t, f x

theorem Finset.sum_ite_index {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (p : Prop) [Decidable p] (s t : Finset ι) (f : ι → M) : ∑ x ∈ if p then s else t, f x = if p then ∑ x ∈ s, f x else ∑ x ∈ t, f x

@[simp]

theorem Finset.prod_ite_irrel {ι : Type u_1} {M : Type u_3} [CommMonoid M] (p : Prop) [Decidable p] (s : Finset ι) (f g : ι → M) : (∏ x ∈ s, if p then f x else g x) = if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x

@[simp]

theorem Finset.sum_ite_irrel {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (p : Prop) [Decidable p] (s : Finset ι) (f g : ι → M) : (∑ x ∈ s, if p then f x else g x) = if p then ∑ x ∈ s, f x else ∑ x ∈ s, g x

@[simp]

theorem Finset.prod_dite_irrel {ι : Type u_1} {M : Type u_3} [CommMonoid M] (p : Prop) [Decidable p] (s : Finset ι) (f : p → ι → M) (g : ¬p → ι → M) : (∏ x ∈ s, if h : p then f h x else g h x) = if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x

@[simp]

theorem Finset.sum_dite_irrel {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (p : Prop) [Decidable p] (s : Finset ι) (f : p → ι → M) (g : ¬p → ι → M) : (∑ x ∈ s, if h : p then f h x else g h x) = if h : p then ∑ x ∈ s, f h x else ∑ x ∈ s, g h x

theorem Finset.ite_prod_one {ι : Type u_1} {M : Type u_3} [CommMonoid M] (p : Prop) [Decidable p] (s : Finset ι) (f : ι → M) : (if p then ∏ x ∈ s, f x else 1) = ∏ x ∈ s, if p then f x else 1

theorem Finset.ite_sum_zero {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (p : Prop) [Decidable p] (s : Finset ι) (f : ι → M) : (if p then ∑ x ∈ s, f x else 0) = ∑ x ∈ s, if p then f x else 0

theorem Finset.ite_one_prod {ι : Type u_1} {M : Type u_3} [CommMonoid M] (p : Prop) [Decidable p] (s : Finset ι) (f : ι → M) : (if p then 1 else ∏ x ∈ s, f x) = ∏ x ∈ s, if p then 1 else f x

theorem Finset.ite_zero_sum {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (p : Prop) [Decidable p] (s : Finset ι) (f : ι → M) : (if p then 0 else ∑ x ∈ s, f x) = ∑ x ∈ s, if p then 0 else f x

theorem Finset.nonempty_of_prod_ne_one {ι : Type u_1} {M : Type u_3} {s : Finset ι} {f : ι → M} [CommMonoid M] (h : ∏ x ∈ s, f x ≠ 1) : s.Nonempty

theorem Finset.nonempty_of_sum_ne_zero {ι : Type u_1} {M : Type u_3} {s : Finset ι} {f : ι → M} [AddCommMonoid M] (h : ∑ x ∈ s, f x ≠ 0) : s.Nonempty

theorem Finset.prod_range_zero {M : Type u_3} [CommMonoid M] (f : ℕ → M) : ∏ k ∈ range 0, f k = 1

theorem Finset.sum_range_zero {M : Type u_3} [AddCommMonoid M] (f : ℕ → M) : ∑ k ∈ range 0, f k = 0

theorem Finset.sum_filter_count_eq_countP {ι : Type u_1} [DecidableEq ι] (p : ι → Prop) [DecidablePred p] (l : List ι) : ∑ x ∈ l.toFinset with p x, List.count x l = List.countP (fun (b : ι) => decide (p b)) l

theorem Finset.prod_mem_multiset {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] (m : Multiset ι) (f : { x : ι // x ∈ m } → M) (g : ι → M) (hfg : ∀ (x : { x : ι // x ∈ m }), f x = g ↑x) : ∏ x : { x : ι // x ∈ m }, f x = ∏ x ∈ m.toFinset, g x

theorem Finset.sum_mem_multiset {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] (m : Multiset ι) (f : { x : ι // x ∈ m } → M) (g : ι → M) (hfg : ∀ (x : { x : ι // x ∈ m }), f x = g ↑x) : ∑ x : { x : ι // x ∈ m }, f x = ∑ x ∈ m.toFinset, g x

theorem Finset.prod_induction {ι : Type u_1} {s : Finset ι} {M : Type u_7} [CommMonoid M] (f : ι → M) (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ s, p (f x)) : p (∏ x ∈ s, f x)

To prove a property of a product, it suffices to prove that the property is multiplicative and holds on factors.

theorem Finset.sum_induction {ι : Type u_1} {s : Finset ι} {M : Type u_7} [AddCommMonoid M] (f : ι → M) (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a + b)) (addUnit : p 0) (base : ∀ x ∈ s, p (f x)) : p (∑ x ∈ s, f x)

To prove a property of a sum, it suffices to prove that the property is additive and holds on summands.

theorem Finset.prod_induction_nonempty {ι : Type u_1} {s : Finset ι} {M : Type u_7} [CommMonoid M] (f : ι → M) (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a * b)) (nonempty : s.Nonempty) (base : ∀ x ∈ s, p (f x)) : p (∏ x ∈ s, f x)

To prove a property of a product, it suffices to prove that the property is multiplicative and holds on factors.

theorem Finset.sum_induction_nonempty {ι : Type u_1} {s : Finset ι} {M : Type u_7} [AddCommMonoid M] (f : ι → M) (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a + b)) (nonempty : s.Nonempty) (base : ∀ x ∈ s, p (f x)) : p (∑ x ∈ s, f x)

To prove a property of a sum, it suffices to prove that the property is additive and holds on summands.

theorem Finset.prod_pow {ι : Type u_1} {M : Type u_3} [CommMonoid M] (s : Finset ι) (n : ℕ) (f : ι → M) : ∏ x ∈ s, f x ^ n = (∏ x ∈ s, f x) ^ n

theorem Finset.sum_nsmul {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (n : ℕ) (f : ι → M) : ∑ x ∈ s, n • f x = n • ∑ x ∈ s, f x

theorem Finset.prod_dvd_prod_of_subset {ι : Type u_7} {M : Type u_8} [CommMonoid M] (s t : Finset ι) (f : ι → M) (h : s ⊆ t) : ∏ i ∈ s, f i ∣ ∏ i ∈ t, f i

@[simp]

theorem Finset.op_sum {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : MulOpposite.op (∑ x ∈ s, f x) = ∑ x ∈ s, MulOpposite.op (f x)

Moving to the opposite additive commutative monoid commutes with summing.

@[simp]

theorem Finset.unop_sum {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → Mᵐᵒᵖ) : MulOpposite.unop (∑ x ∈ s, f x) = ∑ x ∈ s, MulOpposite.unop (f x)

@[simp]

theorem Finset.op_prod {ι : Type u_1} {M : Type u_3} [CommMonoid M] (s : Finset ι) (f : ι → M) : AddOpposite.op (∏ i ∈ s, f i) = ∏ i ∈ s, AddOpposite.op (f i)

@[simp]

theorem Finset.unop_prod {ι : Type u_1} {M : Type u_3} [CommMonoid M] (s : Finset ι) (f : ι → Mᵐᵒᵖ) : AddOpposite.unop (∏ i ∈ s, f i) = ∏ i ∈ s, AddOpposite.unop (f i)

@[simp]

theorem Finset.prod_inv_distrib {ι : Type u_1} {G : Type u_5} {s : Finset ι} [DivisionCommMonoid G] (f : ι → G) : ∏ x ∈ s, (f x)⁻¹ = (∏ x ∈ s, f x)⁻¹

@[simp]

theorem Finset.sum_neg_distrib {ι : Type u_1} {G : Type u_5} {s : Finset ι} [SubtractionCommMonoid G] (f : ι → G) : ∑ x ∈ s, -f x = -∑ x ∈ s, f x

@[simp]

theorem Finset.prod_div_distrib {ι : Type u_1} {G : Type u_5} {s : Finset ι} [DivisionCommMonoid G] (f g : ι → G) : ∏ x ∈ s, f x / g x = (∏ x ∈ s, f x) / ∏ x ∈ s, g x

@[simp]

theorem Finset.sum_sub_distrib {ι : Type u_1} {G : Type u_5} {s : Finset ι} [SubtractionCommMonoid G] (f g : ι → G) : ∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x - ∑ x ∈ s, g x

theorem Finset.prod_zpow {ι : Type u_1} {G : Type u_5} [DivisionCommMonoid G] (f : ι → G) (s : Finset ι) (n : ℤ) : ∏ a ∈ s, f a ^ n = (∏ a ∈ s, f a) ^ n

theorem Finset.sum_zsmul {ι : Type u_1} {G : Type u_5} [SubtractionCommMonoid G] (f : ι → G) (s : Finset ι) (n : ℤ) : ∑ a ∈ s, n • f a = n • ∑ a ∈ s, f a

theorem Finset.sum_nat_mod {ι : Type u_1} (s : Finset ι) (n : ℕ) (f : ι → ℕ) : (∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n

theorem Finset.prod_nat_mod {ι : Type u_1} (s : Finset ι) (n : ℕ) (f : ι → ℕ) : (∏ i ∈ s, f i) % n = (∏ i ∈ s, f i % n) % n

theorem Finset.sum_int_mod {ι : Type u_1} (s : Finset ι) (n : ℤ) (f : ι → ℤ) : (∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n

theorem Finset.prod_int_mod {ι : Type u_1} (s : Finset ι) (n : ℤ) (f : ι → ℤ) : (∏ i ∈ s, f i) % n = (∏ i ∈ s, f i % n) % n

theorem Fintype.prod_bijective {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [CommMonoid M] (e : ι → κ) (he : Function.Bijective e) (f : ι → M) (g : κ → M) (h : ∀ (x : ι), f x = g (e x)) : ∏ x : ι, f x = ∏ x : κ, g x

Fintype.prod_bijective is a variant of Finset.prod_bij that accepts Function.Bijective.

See Function.Bijective.prod_comp for a version without h.

theorem Fintype.sum_bijective {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] (e : ι → κ) (he : Function.Bijective e) (f : ι → M) (g : κ → M) (h : ∀ (x : ι), f x = g (e x)) : ∑ x : ι, f x = ∑ x : κ, g x

Fintype.sum_bijective is a variant of Finset.sum_bij that accepts Function.Bijective.

See Function.Bijective.sum_comp for a version without h.

theorem Function.Bijective.finset_prod {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [CommMonoid M] (e : ι → κ) (he : Bijective e) (f : ι → M) (g : κ → M) (h : ∀ (x : ι), f x = g (e x)) : ∏ x : ι, f x = ∏ x : κ, g x

Alias of Fintype.prod_bijective.

---

Fintype.prod_bijective is a variant of Finset.prod_bij that accepts Function.Bijective.

See Function.Bijective.prod_comp for a version without h.

theorem Function.Bijective.finset_sum {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] (e : ι → κ) (he : Bijective e) (f : ι → M) (g : κ → M) (h : ∀ (x : ι), f x = g (e x)) : ∑ x : ι, f x = ∑ x : κ, g x

theorem Fintype.prod_equiv {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [CommMonoid M] (e : ι ≃ κ) (f : ι → M) (g : κ → M) (h : ∀ (x : ι), f x = g (e x)) : ∏ x : ι, f x = ∏ x : κ, g x

Fintype.prod_equiv is a specialization of Finset.prod_bij that automatically fills in most arguments.

See Equiv.prod_comp for a version without h.

theorem Fintype.sum_equiv {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] (e : ι ≃ κ) (f : ι → M) (g : κ → M) (h : ∀ (x : ι), f x = g (e x)) : ∑ x : ι, f x = ∑ x : κ, g x

Fintype.sum_equiv is a specialization of Finset.sum_bij that automatically fills in most arguments.

See Equiv.sum_comp for a version without h.

theorem Function.Bijective.prod_comp {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [CommMonoid M] {e : ι → κ} (he : Bijective e) (g : κ → M) : ∏ i : ι, g (e i) = ∏ i : κ, g i

theorem Function.Bijective.sum_comp {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] {e : ι → κ} (he : Bijective e) (g : κ → M) : ∑ i : ι, g (e i) = ∑ i : κ, g i

theorem Equiv.prod_comp {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [CommMonoid M] (e : ι ≃ κ) (g : κ → M) : ∏ i : ι, g (e i) = ∏ i : κ, g i

theorem Equiv.sum_comp {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [Fintype ι] [Fintype κ] [AddCommMonoid M] (e : ι ≃ κ) (g : κ → M) : ∑ i : ι, g (e i) = ∑ i : κ, g i

theorem Fintype.prod_empty {ι : Type u_1} {M : Type u_3} [Fintype ι] [CommMonoid M] [IsEmpty ι] (f : ι → M) : ∏ x : ι, f x = 1

theorem Fintype.sum_empty {ι : Type u_1} {M : Type u_3} [Fintype ι] [AddCommMonoid M] [IsEmpty ι] (f : ι → M) : ∑ x : ι, f x = 0

@[simp]

theorem Finset.prod_attach_univ {ι : Type u_1} {M : Type u_3} [CommMonoid M] [Fintype ι] (f : ↥univ → M) : ∏ i ∈ univ.attach, f i = ∏ i : ι, f ⟨i, ⋯⟩

@[simp]

theorem Finset.sum_attach_univ {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [Fintype ι] (f : ↥univ → M) : ∑ i ∈ univ.attach, f i = ∑ i : ι, f ⟨i, ⋯⟩

theorem Finset.prod_erase_attach {ι : Type u_1} {M : Type u_3} [CommMonoid M] [DecidableEq ι] {s : Finset ι} (f : ι → M) (i : ↥s) : ∏ j ∈ s.attach.erase i, f ↑j = ∏ j ∈ s.erase ↑i, f j

theorem Finset.sum_erase_attach {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] [DecidableEq ι] {s : Finset ι} (f : ι → M) (i : ↥s) : ∑ j ∈ s.attach.erase i, f ↑j = ∑ j ∈ s.erase ↑i, f j

@[simp]

theorem Multiset.card_sum {ι : Type u_1} {α : Type u_6} (s : Finset ι) (f : ι → Multiset α) : (∑ i ∈ s, f i).card = ∑ i ∈ s, (f i).card

theorem Multiset.disjoint_list_sum_left {α : Type u_6} {a : Multiset α} {l : List (Multiset α)} : Disjoint l.sum a ↔ ∀ b ∈ l, Disjoint b a

theorem Multiset.disjoint_list_sum_right {α : Type u_6} {a : Multiset α} {l : List (Multiset α)} : Disjoint a l.sum ↔ ∀ b ∈ l, Disjoint a b

theorem Multiset.disjoint_sum_left {α : Type u_6} {a : Multiset α} {i : Multiset (Multiset α)} : Disjoint i.sum a ↔ ∀ b ∈ i, Disjoint b a

theorem Multiset.disjoint_sum_right {α : Type u_6} {a : Multiset α} {i : Multiset (Multiset α)} : Disjoint a i.sum ↔ ∀ b ∈ i, Disjoint a b

theorem Multiset.disjoint_finset_sum_left {ι : Type u_1} {α : Type u_6} {i : Finset ι} {f : ι → Multiset α} {a : Multiset α} : Disjoint (i.sum f) a ↔ ∀ b ∈ i, Disjoint (f b) a

theorem Multiset.disjoint_finset_sum_right {ι : Type u_1} {α : Type u_6} {i : Finset ι} {f : ι → Multiset α} {a : Multiset α} : Disjoint a (i.sum f) ↔ ∀ b ∈ i, Disjoint a (f b)

theorem Multiset.count_sum' {ι : Type u_1} {α : Type u_6} [DecidableEq α] {s : Finset ι} {a : α} {f : ι → Multiset α} : count a (∑ x ∈ s, f x) = ∑ x ∈ s, count a (f x)

theorem Multiset.toFinset_prod_dvd_prod {M : Type u_3} [DecidableEq M] [CommMonoid M] (S : Multiset M) : S.toFinset.prod id ∣ S.prod

@[simp]

theorem Units.coe_prod {M : Type u_3} {α : Type u_6} [CommMonoid M] (f : α → Mˣ) (s : Finset α) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)

Additive, Multiplicative

@[simp]

theorem ofMul_list_prod {M : Type u_3} [Monoid M] (s : List M) : Additive.ofMul s.prod = (List.map (⇑Additive.ofMul) s).sum

@[simp]

theorem toMul_list_sum {M : Type u_3} [Monoid M] (s : List (Additive M)) : Additive.toMul s.sum = (List.map (⇑Additive.toMul) s).prod

@[simp]

theorem ofAdd_list_prod {M : Type u_3} [AddMonoid M] (s : List M) : Multiplicative.ofAdd s.sum = (List.map (⇑Multiplicative.ofAdd) s).prod

@[simp]

theorem toAdd_list_sum {M : Type u_3} [AddMonoid M] (s : List (Multiplicative M)) : Multiplicative.toAdd s.prod = (List.map (⇑Multiplicative.toAdd) s).sum

@[simp]

theorem ofMul_multiset_prod {M : Type u_3} [CommMonoid M] (s : Multiset M) : Additive.ofMul s.prod = (Multiset.map (⇑Additive.ofMul) s).sum

@[simp]

theorem toMul_multiset_sum {M : Type u_3} [CommMonoid M] (s : Multiset (Additive M)) : Additive.toMul s.sum = (Multiset.map (⇑Additive.toMul) s).prod

@[simp]

theorem ofMul_prod {ι : Type u_1} {M : Type u_3} [CommMonoid M] (s : Finset ι) (f : ι → M) : Additive.ofMul (∏ i ∈ s, f i) = ∑ i ∈ s, Additive.ofMul (f i)

@[simp]

theorem toMul_sum {ι : Type u_1} {M : Type u_3} [CommMonoid M] (s : Finset ι) (f : ι → Additive M) : Additive.toMul (∑ i ∈ s, f i) = ∏ i ∈ s, Additive.toMul (f i)

@[simp]

theorem ofAdd_multiset_prod {M : Type u_3} [AddCommMonoid M] (s : Multiset M) : Multiplicative.ofAdd s.sum = (Multiset.map (⇑Multiplicative.ofAdd) s).prod

@[simp]

theorem toAdd_multiset_sum {M : Type u_3} [AddCommMonoid M] (s : Multiset (Multiplicative M)) : Multiplicative.toAdd s.prod = (Multiset.map (⇑Multiplicative.toAdd) s).sum

@[simp]

theorem ofAdd_sum {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : Multiplicative.ofAdd (∑ i ∈ s, f i) = ∏ i ∈ s, Multiplicative.ofAdd (f i)

@[simp]

theorem toAdd_prod {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → Multiplicative M) : Multiplicative.toAdd (∏ i ∈ s, f i) = ∑ i ∈ s, Multiplicative.toAdd (f i)