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_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : α → β) : β

∏ 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_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : β

∑ 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_3} {β : Type u_4} [CommMonoid β] (s : Multiset α) (hs : s.Nodup) (f : α → β) : { val := s, nodup := hs }.prod f = (Multiset.map f s).prod

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Collect 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) (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" 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) (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" term)? "," term

def BigOperators.bigsumin : Lean.ParserDescr

Deprecated, use ∑ x ∈ s, f x instead.

def BigOperators.bigprodin : Lean.ParserDescr

Deprecated, use ∏ x ∈ s, f x instead.

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_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : α → β) : ∏ x ∈ s, f x = (Multiset.map f s.val).prod

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem map_prod {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] [CommMonoid γ] {G : Type u_6} [FunLike G β γ] [MonoidHomClass G β γ] (g : G) (f : α → β) (s : Finset α) : g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)

@[simp]

theorem map_sum {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] [AddCommMonoid γ] {G : Type u_6} [FunLike G β γ] [AddMonoidHomClass G β γ] (g : G) (f : α → β) (s : Finset α) : g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x)

@[simp]

theorem Finset.prod_empty {α : Type u_3} {β : Type u_4} {f : α → β} [CommMonoid β] : ∏ x ∈ ∅, f x = 1

@[simp]

theorem Finset.sum_empty {α : Type u_3} {β : Type u_4} {f : α → β} [AddCommMonoid β] : ∑ x ∈ ∅, f x = 0

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

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

@[simp]

theorem Finset.prod_const_one {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] : ∏ _x ∈ s, 1 = 1

@[simp]

theorem Finset.sum_const_zero {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] : ∑ _x ∈ s, 0 = 0

@[simp]

theorem Finset.prod_map {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset α) (e : α ↪ γ) (f : γ → β) : ∏ x ∈ map e s, f x = ∏ x ∈ s, f (e x)

@[simp]

theorem Finset.sum_map {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset α) (e : α ↪ γ) (f : γ → β) : ∑ x ∈ map e s, f x = ∑ x ∈ s, f (e x)

@[simp]

theorem Finset.prod_map_toList {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : α → β) : (List.map f s.toList).prod = s.prod f

@[simp]

theorem Finset.sum_map_toList {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : (List.map f s.toList).sum = s.sum f

@[deprecated Finset.prod_map_toList (since := "2025-04-09")]

theorem Finset.prod_to_list {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : α → β) : (List.map f s.toList).prod = s.prod f

Alias of Finset.prod_map_toList.

@[deprecated Finset.sum_map_toList (since := "2025-04-09")]

theorem Finset.sum_to_list {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : (List.map f s.toList).sum = s.sum f

Alias of Finset.sum_map_toList.

@[simp]

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

@[simp]

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

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

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

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

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

theorem Finset.prod_bij {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (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_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (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_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (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_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (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 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_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (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_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (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_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (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_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (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 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_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (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_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (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_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (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_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (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_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] [CommMonoid γ] {r : β → γ → Prop} {f : α → β} {g : α → γ} {s : Finset α} (h₁ : r 1 1) (h₂ : ∀ (a : α) (b : β) (c : γ), 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_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] [AddCommMonoid γ] {r : β → γ → Prop} {f : α → β} {g : α → γ} {s : Finset α} (h₁ : r 0 0) (h₂ : ∀ (a : α) (b : β) (c : γ), 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_3} {β : Type u_4} (s : Finset α) [CommMonoid β] (f : { x : α // x ∈ s } → β) : ∏ i : { x : α // x ∈ s }, f i = ∏ i ∈ s.attach, f i

theorem Finset.sum_coe_sort_eq_attach {α : Type u_3} {β : Type u_4} (s : Finset α) [AddCommMonoid β] (f : { x : α // x ∈ s } → β) : ∑ i : { x : α // x ∈ s }, f i = ∑ i ∈ s.attach, f i

theorem Finset.prod_ite_index {α : Type u_3} {β : Type u_4} [CommMonoid β] (p : Prop) [Decidable p] (s t : Finset α) (f : α → β) : ∏ 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_3} {β : Type u_4} [AddCommMonoid β] (p : Prop) [Decidable p] (s t : Finset α) (f : α → β) : ∑ 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_3} {β : Type u_4} [CommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f g : α → β) : (∏ 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_3} {β : Type u_4} [AddCommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f g : α → β) : (∑ 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_3} {β : Type u_4} [CommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f : p → α → β) (g : ¬p → α → β) : (∏ 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_3} {β : Type u_4} [AddCommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f : p → α → β) (g : ¬p → α → β) : (∑ 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_3} {β : Type u_4} [CommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f : α → β) : (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_3} {β : Type u_4} [AddCommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f : α → β) : (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_3} {β : Type u_4} [CommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f : α → β) : (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_3} {β : Type u_4} [AddCommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f : α → β) : (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_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] (h : ∏ x ∈ s, f x ≠ 1) : s.Nonempty

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

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

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

theorem Finset.sum_filter_count_eq_countP {α : Type u_3} [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_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (m : Multiset α) (f : { x : α // x ∈ m } → β) (g : α → β) (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_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (m : Multiset α) (f : { x : α // x ∈ m } → β) (g : α → β) (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_3} {s : Finset α} {M : Type u_6} [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_3} {s : Finset α} {M : Type u_6} [AddCommMonoid M] (f : α → M) (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a + b)) (unit : 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_3} {s : Finset α} {M : Type u_6} [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_3} {s : Finset α} {M : Type u_6} [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_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (n : ℕ) (f : α → β) : ∏ x ∈ s, f x ^ n = (∏ x ∈ s, f x) ^ n

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

theorem Finset.prod_dvd_prod_of_subset {ι : Type u_6} {M : Type u_7} [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_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} (f : α → β) : 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_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} (f : α → βᵐᵒᵖ) : MulOpposite.unop (∑ x ∈ s, f x) = ∑ x ∈ s, MulOpposite.unop (f x)

@[simp]

theorem Finset.prod_inv_distrib {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [DivisionCommMonoid β] : ∏ x ∈ s, (f x)⁻¹ = (∏ x ∈ s, f x)⁻¹

@[simp]

theorem Finset.sum_neg_distrib {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [SubtractionCommMonoid β] : ∑ x ∈ s, -f x = -∑ x ∈ s, f x

@[simp]

theorem Finset.prod_div_distrib {α : Type u_3} {β : Type u_4} {s : Finset α} {f g : α → β} [DivisionCommMonoid β] : ∏ x ∈ s, f x / g x = (∏ x ∈ s, f x) / ∏ x ∈ s, g x

@[simp]

theorem Finset.sum_sub_distrib {α : Type u_3} {β : Type u_4} {s : Finset α} {f g : α → β} [SubtractionCommMonoid β] : ∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x - ∑ x ∈ s, g x

theorem Finset.prod_zpow {α : Type u_3} {β : Type u_4} [DivisionCommMonoid β] (f : α → β) (s : Finset α) (n : ℤ) : ∏ a ∈ s, f a ^ n = (∏ a ∈ s, f a) ^ n

theorem Finset.sum_zsmul {α : Type u_3} {β : Type u_4} [SubtractionCommMonoid β] (f : α → β) (s : Finset α) (n : ℤ) : ∑ a ∈ s, n • f a = n • ∑ a ∈ s, f a

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

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

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

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

theorem Fintype.prod_bijective {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommMonoid α] (e : ι → κ) (he : Function.Bijective e) (f : ι → α) (g : κ → α) (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_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] (e : ι → κ) (he : Function.Bijective e) (f : ι → α) (g : κ → α) (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_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommMonoid α] (e : ι → κ) (he : Bijective e) (f : ι → α) (g : κ → α) (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_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] (e : ι → κ) (he : Bijective e) (f : ι → α) (g : κ → α) (h : ∀ (x : ι), f x = g (e x)) : ∑ x : ι, f x = ∑ x : κ, g x

theorem Fintype.prod_equiv {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommMonoid α] (e : ι ≃ κ) (f : ι → α) (g : κ → α) (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_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] (e : ι ≃ κ) (f : ι → α) (g : κ → α) (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_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommMonoid α] {e : ι → κ} (he : Bijective e) (g : κ → α) : ∏ i : ι, g (e i) = ∏ i : κ, g i

theorem Function.Bijective.sum_comp {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] {e : ι → κ} (he : Bijective e) (g : κ → α) : ∑ i : ι, g (e i) = ∑ i : κ, g i

theorem Equiv.prod_comp {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommMonoid α] (e : ι ≃ κ) (g : κ → α) : ∏ i : ι, g (e i) = ∏ i : κ, g i

theorem Equiv.sum_comp {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] (e : ι ≃ κ) (g : κ → α) : ∑ i : ι, g (e i) = ∑ i : κ, g i

theorem Fintype.prod_empty {α : Type u_9} {β : Type u_10} [CommMonoid β] [IsEmpty α] [Fintype α] (f : α → β) : ∏ x : α, f x = 1

theorem Fintype.sum_empty {α : Type u_9} {β : Type u_10} [AddCommMonoid β] [IsEmpty α] [Fintype α] (f : α → β) : ∑ x : α, f x = 0

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

theorem Multiset.disjoint_finset_sum_left {α : Type u_3} {β : 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_3} {β : 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_3} {β : Type u_4} [DecidableEq α] {s : Finset β} {a : α} {f : β → Multiset α} : count a (∑ x ∈ s, f x) = ∑ x ∈ s, count a (f x)

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

@[simp]

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

Additive, Multiplicative

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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