Big operators

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

Notation

We introduce the following notation, localized in BigOperators. To enable the notation, use open BigOperators.

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)

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.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.

Equations

• s.sum f = (Multiset.map f s.val).sum

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.

Equations

• s.prod f = (Multiset.map f s.val).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_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_val {α : Type u_3} [AddCommMonoid α] (s : Finset α) : s.val.sum = s.sum id

@[simp]

theorem Finset.prod_val {α : Type u_3} [CommMonoid α] (s : Finset α) : s.val.prod = s.prod 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.

Equations

• One or more equations did not get rendered due to their size.

def BigOperators.bigOpBinderParenthesized : Lean.ParserDescr

A BigOperator binder in parentheses

Equations

• One or more equations did not get rendered due to their size.

def BigOperators.bigOpBinderCollection : Lean.ParserDescr

A list of parenthesized binders

Equations

• One or more equations did not get rendered due to their size.

def BigOperators.bigOpBinders : Lean.ParserDescr

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Collects the binder/Finset pairs for the given bigOpBinders.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Collect the terms into a product of sets.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def BigOperators.bigsumin : Lean.ParserDescr

(Deprecated, use ∑ x ∈ s, f x) ∑ x in 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.

Equations

• One or more equations did not get rendered due to their size.

def BigOperators.bigprodin : Lean.ParserDescr

(Deprecated, use ∏ x ∈ s, f x) ∏ x in 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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• One or more equations did not get rendered due to their size.

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

theorem Finset.prod_eq_multiset_prod {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : α → β) : (s.prod fun (x : α) => f x) = (Multiset.map f s.val).prod

@[simp]

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

@[simp]

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

theorem Finset.sum_eq_fold {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : (s.sum fun (x : α) => f x) = Finset.fold (fun (x x_1 : β) => x + x_1) 0 f s

theorem Finset.prod_eq_fold {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : α → β) : (s.prod fun (x : α) => f x) = Finset.fold (fun (x x_1 : β) => x * x_1) 1 f s

@[simp]

theorem Finset.sum_multiset_singleton {α : Type u_3} (s : Finset α) : (s.sum fun (x : α) => {x}) = s.val

@[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 (s.sum fun (x : α) => f x) = s.sum fun (x : α) => g (f x)

@[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 (s.prod fun (x : α) => f x) = s.prod fun (x : α) => g (f x)

theorem AddMonoidHom.coe_finset_sum {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddZeroClass β] [AddCommMonoid γ] (f : α → β →+ γ) (s : Finset α) : ⇑(s.sum fun (x : α) => f x) = s.sum fun (x : α) => ⇑(f x)

theorem MonoidHom.coe_finset_prod {α : Type u_3} {β : Type u_4} {γ : Type u_5} [MulOneClass β] [CommMonoid γ] (f : α → β →* γ) (s : Finset α) : ⇑(s.prod fun (x : α) => f x) = s.prod fun (x : α) => ⇑(f x)

@[simp]

theorem AddMonoidHom.finset_sum_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddZeroClass β] [AddCommMonoid γ] (f : α → β →+ γ) (s : Finset α) (b : β) : (s.sum fun (x : α) => f x) b = s.sum fun (x : α) => (f x) b

See also Finset.sum_apply, with the same conclusion but with the weaker hypothesis f : α → β → γ

@[simp]

theorem MonoidHom.finset_prod_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [MulOneClass β] [CommMonoid γ] (f : α → β →* γ) (s : Finset α) (b : β) : (s.prod fun (x : α) => f x) b = s.prod fun (x : α) => (f x) b

See also Finset.prod_apply, with the same conclusion but with the weaker hypothesis f : α → β → γ

@[simp]

theorem Finset.sum_empty {α : Type u_3} {β : Type u_4} {f : α → β} [AddCommMonoid β] : (∅.sum fun (x : α) => f x) = 0

@[simp]

theorem Finset.prod_empty {α : Type u_3} {β : Type u_4} {f : α → β} [CommMonoid β] : (∅.prod fun (x : α) => f x) = 1

theorem Finset.sum_of_empty {α : Type u_3} {β : Type u_4} {f : α → β} [AddCommMonoid β] [IsEmpty α] (s : Finset α) : (s.sum fun (i : α) => f i) = 0

theorem Finset.prod_of_empty {α : Type u_3} {β : Type u_4} {f : α → β} [CommMonoid β] [IsEmpty α] (s : Finset α) : (s.prod fun (i : α) => f i) = 1

@[simp]

theorem Finset.sum_cons {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [AddCommMonoid β] (h : a ∉ s) : ((Finset.cons a s h).sum fun (x : α) => f x) = f a + s.sum fun (x : α) => f x

@[simp]

theorem Finset.prod_cons {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [CommMonoid β] (h : a ∉ s) : ((Finset.cons a s h).prod fun (x : α) => f x) = f a * s.prod fun (x : α) => f x

@[simp]

theorem Finset.sum_insert {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [AddCommMonoid β] [DecidableEq α] : a ∉ s → ((insert a s).sum fun (x : α) => f x) = f a + s.sum fun (x : α) => f x

@[simp]

theorem Finset.prod_insert {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [CommMonoid β] [DecidableEq α] : a ∉ s → ((insert a s).prod fun (x : α) => f x) = f a * s.prod fun (x : α) => f x

@[simp]

theorem Finset.sum_insert_of_eq_zero_if_not_mem {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [AddCommMonoid β] [DecidableEq α] (h : a ∉ s → f a = 0) : ((insert a s).sum fun (x : α) => f x) = s.sum fun (x : α) => f x

The sum of f over insert a s is the same as the sum over s, as long as a is in s or f a = 0.

@[simp]

theorem Finset.prod_insert_of_eq_one_if_not_mem {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [CommMonoid β] [DecidableEq α] (h : a ∉ s → f a = 1) : ((insert a s).prod fun (x : α) => f x) = s.prod fun (x : α) => f x

The product of f over insert a s is the same as the product over s, as long as a is in s or f a = 1.

@[simp]

theorem Finset.sum_insert_zero {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [AddCommMonoid β] [DecidableEq α] (h : f a = 0) : ((insert a s).sum fun (x : α) => f x) = s.sum fun (x : α) => f x

The sum of f over insert a s is the same as the sum over s, as long as f a = 0.

@[simp]

theorem Finset.prod_insert_one {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [CommMonoid β] [DecidableEq α] (h : f a = 1) : ((insert a s).prod fun (x : α) => f x) = s.prod fun (x : α) => f x

The product of f over insert a s is the same as the product over s, as long as f a = 1.

theorem Finset.sum_insert_sub {α : Type u_3} {s : Finset α} {a : α} {M : Type u_6} [AddCommGroup M] [DecidableEq α] (ha : a ∉ s) {f : α → M} : ((insert a s).sum fun (x : α) => f x) - f a = s.sum fun (x : α) => f x

theorem Finset.prod_insert_div {α : Type u_3} {s : Finset α} {a : α} {M : Type u_6} [CommGroup M] [DecidableEq α] (ha : a ∉ s) {f : α → M} : ((insert a s).prod fun (x : α) => f x) / f a = s.prod fun (x : α) => f x

@[simp]

theorem Finset.sum_singleton {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (f : α → β) (a : α) : ({a}.sum fun (x : α) => f x) = f a

@[simp]

theorem Finset.prod_singleton {α : Type u_3} {β : Type u_4} [CommMonoid β] (f : α → β) (a : α) : ({a}.prod fun (x : α) => f x) = f a

theorem Finset.sum_pair {α : Type u_3} {β : Type u_4} {f : α → β} [AddCommMonoid β] [DecidableEq α] {a : α} {b : α} (h : a ≠ b) : ({a, b}.sum fun (x : α) => f x) = f a + f b

theorem Finset.prod_pair {α : Type u_3} {β : Type u_4} {f : α → β} [CommMonoid β] [DecidableEq α] {a : α} {b : α} (h : a ≠ b) : ({a, b}.prod fun (x : α) => f x) = f a * f b

@[simp]

theorem Finset.sum_const_zero {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] : (s.sum fun (_x : α) => 0) = 0

@[simp]

theorem Finset.prod_const_one {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] : (s.prod fun (_x : α) => 1) = 1

@[simp]

theorem Finset.sum_image {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β} [AddCommMonoid β] [DecidableEq α] {s : Finset γ} {g : γ → α} : (∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) → ((Finset.image g s).sum fun (x : α) => f x) = s.sum fun (x : γ) => f (g x)

@[simp]

theorem Finset.prod_image {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β} [CommMonoid β] [DecidableEq α] {s : Finset γ} {g : γ → α} : (∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) → ((Finset.image g s).prod fun (x : α) => f x) = s.prod fun (x : γ) => f (g x)

@[simp]

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

@[simp]

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

theorem Finset.sum_attach {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : (s.attach.sum fun (x : { x : α // x ∈ s }) => f ↑x) = s.sum fun (x : α) => f x

theorem Finset.prod_attach {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : α → β) : (s.attach.prod fun (x : { x : α // x ∈ s }) => f ↑x) = s.prod fun (x : α) => f x

theorem Finset.sum_congr {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} {g : α → β} [AddCommMonoid β] (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.sum f = s₂.sum g

theorem Finset.prod_congr {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} {g : α → β} [CommMonoid β] (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g

theorem Finset.sum_eq_zero {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {f : α → β} {s : Finset α} (h : ∀ x ∈ s, f x = 0) : (s.sum fun (x : α) => f x) = 0

theorem Finset.prod_eq_one {α : Type u_3} {β : Type u_4} [CommMonoid β] {f : α → β} {s : Finset α} (h : ∀ x ∈ s, f x = 1) : (s.prod fun (x : α) => f x) = 1

theorem Finset.sum_disjUnion {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [AddCommMonoid β] (h : Disjoint s₁ s₂) : ((s₁.disjUnion s₂ h).sum fun (x : α) => f x) = (s₁.sum fun (x : α) => f x) + s₂.sum fun (x : α) => f x

theorem Finset.prod_disjUnion {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [CommMonoid β] (h : Disjoint s₁ s₂) : ((s₁.disjUnion s₂ h).prod fun (x : α) => f x) = (s₁.prod fun (x : α) => f x) * s₂.prod fun (x : α) => f x

theorem Finset.sum_disjiUnion {ι : Type u_1} {α : Type u_3} {β : Type u_4} {f : α → β} [AddCommMonoid β] (s : Finset ι) (t : ι → Finset α) (h : (↑s).PairwiseDisjoint t) : ((s.disjiUnion t h).sum fun (x : α) => f x) = s.sum fun (i : ι) => (t i).sum fun (x : α) => f x

theorem Finset.prod_disjiUnion {ι : Type u_1} {α : Type u_3} {β : Type u_4} {f : α → β} [CommMonoid β] (s : Finset ι) (t : ι → Finset α) (h : (↑s).PairwiseDisjoint t) : ((s.disjiUnion t h).prod fun (x : α) => f x) = s.prod fun (i : ι) => (t i).prod fun (x : α) => f x

theorem Finset.sum_union_inter {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [AddCommMonoid β] [DecidableEq α] : (((s₁ ∪ s₂).sum fun (x : α) => f x) + (s₁ ∩ s₂).sum fun (x : α) => f x) = (s₁.sum fun (x : α) => f x) + s₂.sum fun (x : α) => f x

theorem Finset.prod_union_inter {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [CommMonoid β] [DecidableEq α] : (((s₁ ∪ s₂).prod fun (x : α) => f x) * (s₁ ∩ s₂).prod fun (x : α) => f x) = (s₁.prod fun (x : α) => f x) * s₂.prod fun (x : α) => f x

theorem Finset.sum_union {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [AddCommMonoid β] [DecidableEq α] (h : Disjoint s₁ s₂) : ((s₁ ∪ s₂).sum fun (x : α) => f x) = (s₁.sum fun (x : α) => f x) + s₂.sum fun (x : α) => f x

theorem Finset.prod_union {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [CommMonoid β] [DecidableEq α] (h : Disjoint s₁ s₂) : ((s₁ ∪ s₂).prod fun (x : α) => f x) = (s₁.prod fun (x : α) => f x) * s₂.prod fun (x : α) => f x

theorem Finset.sum_filter_add_sum_filter_not {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] (f : α → β) : (((Finset.filter p s).sum fun (x : α) => f x) + (Finset.filter (fun (x : α) => ¬p x) s).sum fun (x : α) => f x) = s.sum fun (x : α) => f x

theorem Finset.prod_filter_mul_prod_filter_not {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] (f : α → β) : (((Finset.filter p s).prod fun (x : α) => f x) * (Finset.filter (fun (x : α) => ¬p x) s).prod fun (x : α) => f x) = s.prod fun (x : α) => f x

@[simp]

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

@[simp]

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

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

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

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

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

theorem Finset.sum_powerset_insert {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} [AddCommMonoid β] [DecidableEq α] (ha : a ∉ s) (f : Finset α → β) : ((insert a s).powerset.sum fun (t : Finset α) => f t) = (s.powerset.sum fun (t : Finset α) => f t) + s.powerset.sum fun (t : Finset α) => f (insert a t)

A sum over all subsets of s ∪ {x} is obtained by summing the sum over all subsets of s, and over all subsets of s to which one adds x.

theorem Finset.prod_powerset_insert {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} [CommMonoid β] [DecidableEq α] (ha : a ∉ s) (f : Finset α → β) : ((insert a s).powerset.prod fun (t : Finset α) => f t) = (s.powerset.prod fun (t : Finset α) => f t) * s.powerset.prod fun (t : Finset α) => f (insert a t)

A product over all subsets of s ∪ {x} is obtained by multiplying the product over all subsets of s, and over all subsets of s to which one adds x.

theorem Finset.sum_powerset_cons {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} [AddCommMonoid β] (ha : a ∉ s) (f : Finset α → β) : ((Finset.cons a s ha).powerset.sum fun (t : Finset α) => f t) = (s.powerset.sum fun (t : Finset α) => f t) + s.powerset.attach.sum fun (t : { x : Finset α // x ∈ s.powerset }) => f (Finset.cons a ↑t ⋯)

A sum over all subsets of s ∪ {x} is obtained by summing the sum over all subsets of s, and over all subsets of s to which one adds x.

theorem Finset.prod_powerset_cons {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} [CommMonoid β] (ha : a ∉ s) (f : Finset α → β) : ((Finset.cons a s ha).powerset.prod fun (t : Finset α) => f t) = (s.powerset.prod fun (t : Finset α) => f t) * s.powerset.attach.prod fun (t : { x : Finset α // x ∈ s.powerset }) => f (Finset.cons a ↑t ⋯)

A product over all subsets of s ∪ {x} is obtained by multiplying the product over all subsets of s, and over all subsets of s to which one adds x.

theorem Finset.sum_powerset {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : Finset α → β) : (s.powerset.sum fun (t : Finset α) => f t) = (Finset.range (s.card + 1)).sum fun (j : ℕ) => (Finset.powersetCard j s).sum fun (t : Finset α) => f t

A sum over powerset s is equal to the double sum over sets of subsets of s with card s = k, for k = 1, ..., card s

theorem Finset.prod_powerset {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : Finset α → β) : (s.powerset.prod fun (t : Finset α) => f t) = (Finset.range (s.card + 1)).prod fun (j : ℕ) => (Finset.powersetCard j s).prod fun (t : Finset α) => f t

A product over powerset s is equal to the double product over sets of subsets of s with card s = k, for k = 1, ..., card s.

theorem IsCompl.sum_add_sum {α : Type u_3} {β : Type u_4} [Fintype α] [AddCommMonoid β] {s : Finset α} {t : Finset α} (h : IsCompl s t) (f : α → β) : ((s.sum fun (i : α) => f i) + t.sum fun (i : α) => f i) = Finset.univ.sum fun (i : α) => f i

theorem IsCompl.prod_mul_prod {α : Type u_3} {β : Type u_4} [Fintype α] [CommMonoid β] {s : Finset α} {t : Finset α} (h : IsCompl s t) (f : α → β) : ((s.prod fun (i : α) => f i) * t.prod fun (i : α) => f i) = Finset.univ.prod fun (i : α) => f i

theorem Finset.sum_add_sum_compl {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [Fintype α] [DecidableEq α] (s : Finset α) (f : α → β) : ((s.sum fun (i : α) => f i) + sᶜ.sum fun (i : α) => f i) = Finset.univ.sum fun (i : α) => f i

Adding the sums of a function over s and over sᶜ gives the whole sum. For a version expressed with subtypes, see Fintype.sum_subtype_add_sum_subtype.

theorem Finset.prod_mul_prod_compl {α : Type u_3} {β : Type u_4} [CommMonoid β] [Fintype α] [DecidableEq α] (s : Finset α) (f : α → β) : ((s.prod fun (i : α) => f i) * sᶜ.prod fun (i : α) => f i) = Finset.univ.prod fun (i : α) => f i

Multiplying the products of a function over s and over sᶜ gives the whole product. For a version expressed with subtypes, see Fintype.prod_subtype_mul_prod_subtype.

theorem Finset.sum_compl_add_sum {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [Fintype α] [DecidableEq α] (s : Finset α) (f : α → β) : ((sᶜ.sum fun (i : α) => f i) + s.sum fun (i : α) => f i) = Finset.univ.sum fun (i : α) => f i

theorem Finset.prod_compl_mul_prod {α : Type u_3} {β : Type u_4} [CommMonoid β] [Fintype α] [DecidableEq α] (s : Finset α) (f : α → β) : ((sᶜ.prod fun (i : α) => f i) * s.prod fun (i : α) => f i) = Finset.univ.prod fun (i : α) => f i

theorem Finset.sum_sdiff {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [AddCommMonoid β] [DecidableEq α] (h : s₁ ⊆ s₂) : (((s₂ \ s₁).sum fun (x : α) => f x) + s₁.sum fun (x : α) => f x) = s₂.sum fun (x : α) => f x

theorem Finset.prod_sdiff {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [CommMonoid β] [DecidableEq α] (h : s₁ ⊆ s₂) : (((s₂ \ s₁).prod fun (x : α) => f x) * s₁.prod fun (x : α) => f x) = s₂.prod fun (x : α) => f x

theorem Finset.sum_subset_zero_on_sdiff {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} {g : α → β} [AddCommMonoid β] [DecidableEq α] (h : s₁ ⊆ s₂) (hg : ∀ x ∈ s₂ \ s₁, g x = 0) (hfg : ∀ x ∈ s₁, f x = g x) : (s₁.sum fun (i : α) => f i) = s₂.sum fun (i : α) => g i

theorem Finset.prod_subset_one_on_sdiff {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} {g : α → β} [CommMonoid β] [DecidableEq α] (h : s₁ ⊆ s₂) (hg : ∀ x ∈ s₂ \ s₁, g x = 1) (hfg : ∀ x ∈ s₁, f x = g x) : (s₁.prod fun (i : α) => f i) = s₂.prod fun (i : α) => g i

theorem Finset.sum_subset {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [AddCommMonoid β] (h : s₁ ⊆ s₂) (hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 0) : (s₁.sum fun (x : α) => f x) = s₂.sum fun (x : α) => f x

theorem Finset.prod_subset {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [CommMonoid β] (h : s₁ ⊆ s₂) (hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 1) : (s₁.prod fun (x : α) => f x) = s₂.prod fun (x : α) => f x

@[simp]

theorem Finset.sum_disj_sum {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset α) (t : Finset γ) (f : α ⊕ γ → β) : ((s.disjSum t).sum fun (x : α ⊕ γ) => f x) = (s.sum fun (x : α) => f (Sum.inl x)) + t.sum fun (x : γ) => f (Sum.inr x)

@[simp]

theorem Finset.prod_disj_sum {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset α) (t : Finset γ) (f : α ⊕ γ → β) : ((s.disjSum t).prod fun (x : α ⊕ γ) => f x) = (s.prod fun (x : α) => f (Sum.inl x)) * t.prod fun (x : γ) => f (Sum.inr x)

theorem Finset.sum_sum_elim {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset α) (t : Finset γ) (f : α → β) (g : γ → β) : ((s.disjSum t).sum fun (x : α ⊕ γ) => Sum.elim f g x) = (s.sum fun (x : α) => f x) + t.sum fun (x : γ) => g x

theorem Finset.prod_sum_elim {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset α) (t : Finset γ) (f : α → β) (g : γ → β) : ((s.disjSum t).prod fun (x : α ⊕ γ) => Sum.elim f g x) = (s.prod fun (x : α) => f x) * t.prod fun (x : γ) => g x

theorem Finset.sum_biUnion {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β} [AddCommMonoid β] [DecidableEq α] {s : Finset γ} {t : γ → Finset α} (hs : (↑s).PairwiseDisjoint t) : ((s.biUnion t).sum fun (x : α) => f x) = s.sum fun (x : γ) => (t x).sum fun (i : α) => f i

theorem Finset.prod_biUnion {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β} [CommMonoid β] [DecidableEq α] {s : Finset γ} {t : γ → Finset α} (hs : (↑s).PairwiseDisjoint t) : ((s.biUnion t).prod fun (x : α) => f x) = s.prod fun (x : γ) => (t x).prod fun (i : α) => f i

theorem Finset.sum_sigma {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : Sigma σ → β) : ((s.sigma t).sum fun (x : (i : α) × σ i) => f x) = s.sum fun (a : α) => (t a).sum fun (s : σ a) => f ⟨a, s⟩

Sum over a sigma type equals the sum of fiberwise sums. For rewriting in the reverse direction, use Finset.sum_sigma'

theorem Finset.prod_sigma {α : Type u_3} {β : Type u_4} [CommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : Sigma σ → β) : ((s.sigma t).prod fun (x : (i : α) × σ i) => f x) = s.prod fun (a : α) => (t a).prod fun (s : σ a) => f ⟨a, s⟩

Product over a sigma type equals the product of fiberwise products. For rewriting in the reverse direction, use Finset.prod_sigma'.

theorem Finset.sum_sigma' {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : (a : α) → σ a → β) : (s.sum fun (a : α) => (t a).sum fun (s : σ a) => f a s) = (s.sigma t).sum fun (x : (i : α) × σ i) => f x.fst x.snd

theorem Finset.prod_sigma' {α : Type u_3} {β : Type u_4} [CommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : (a : α) → σ a → β) : (s.prod fun (a : α) => (t a).prod fun (s : σ a) => f a s) = (s.sigma t).prod fun (x : (i : α) × σ i) => f x.fst x.snd

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)) : (s.sum fun (x : ι) => f x) = t.sum fun (x : κ) => 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 → κ) (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)) : (s.prod fun (x : ι) => f x) = t.prod fun (x : κ) => 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 → κ) (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)) : (s.sum fun (x : ι) => f x) = t.sum fun (x : κ) => 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_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)) : (s.prod fun (x : ι) => f x) = t.prod fun (x : κ) => 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_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)) : (s.sum fun (x : ι) => f x) = t.sum fun (x : κ) => 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 : ι → κ) (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)) : (s.prod fun (x : ι) => f x) = t.prod fun (x : κ) => 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 : ι → κ) (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)) : (s.sum fun (x : ι) => f x) = t.sum fun (x : κ) => 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_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)) : (s.prod fun (x : ι) => f x) = t.prod fun (x : κ) => 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_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)) : (s.sum fun (i : ι) => f i) = t.sum fun (i : κ) => 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_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)) : (s.prod fun (i : ι) => f i) = t.prod fun (i : κ) => 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_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)) : (s.sum fun (i : ι) => f i) = t.sum fun (i : κ) => 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_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)) : (s.prod fun (i : ι) => f i) = t.prod fun (i : κ) => 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_of_injOn {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (e : ι → κ) (he : Set.InjOn e ↑s) (hest : Set.MapsTo e ↑s ↑t) (h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 0) (h : ∀ i ∈ s, f i = g (e i)) : (s.sum fun (i : ι) => f i) = t.sum fun (j : κ) => g j

theorem Finset.prod_of_injOn {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (e : ι → κ) (he : Set.InjOn e ↑s) (hest : Set.MapsTo e ↑s ↑t) (h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1) (h : ∀ i ∈ s, f i = g (e i)) : (s.prod fun (i : ι) => f i) = t.prod fun (j : κ) => g j

theorem Finset.sum_fiberwise_eq_sum_filter {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : ι → α) : (t.sum fun (j : κ) => (Finset.filter (fun (i : ι) => g i = j) s).sum fun (i : ι) => f i) = (Finset.filter (fun (i : ι) => g i ∈ t) s).sum fun (i : ι) => f i

theorem Finset.prod_fiberwise_eq_prod_filter {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : ι → α) : (t.prod fun (j : κ) => (Finset.filter (fun (i : ι) => g i = j) s).prod fun (i : ι) => f i) = (Finset.filter (fun (i : ι) => g i ∈ t) s).prod fun (i : ι) => f i

theorem Finset.sum_fiberwise_eq_sum_filter' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : κ → α) : (t.sum fun (j : κ) => (Finset.filter (fun (i : ι) => g i = j) s).sum fun (_i : ι) => f j) = (Finset.filter (fun (i : ι) => g i ∈ t) s).sum fun (i : ι) => f (g i)

theorem Finset.prod_fiberwise_eq_prod_filter' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : κ → α) : (t.prod fun (j : κ) => (Finset.filter (fun (i : ι) => g i = j) s).prod fun (_i : ι) => f j) = (Finset.filter (fun (i : ι) => g i ∈ t) s).prod fun (i : ι) => f (g i)

theorem Finset.sum_fiberwise_of_maps_to {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : ι → α) : (t.sum fun (j : κ) => (Finset.filter (fun (i : ι) => g i = j) s).sum fun (i : ι) => f i) = s.sum fun (i : ι) => f i

theorem Finset.prod_fiberwise_of_maps_to {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : ι → α) : (t.prod fun (j : κ) => (Finset.filter (fun (i : ι) => g i = j) s).prod fun (i : ι) => f i) = s.prod fun (i : ι) => f i

theorem Finset.sum_fiberwise_of_maps_to' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : κ → α) : (t.sum fun (j : κ) => (Finset.filter (fun (i : ι) => g i = j) s).sum fun (_i : ι) => f j) = s.sum fun (i : ι) => f (g i)

theorem Finset.prod_fiberwise_of_maps_to' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : κ → α) : (t.prod fun (j : κ) => (Finset.filter (fun (i : ι) => g i = j) s).prod fun (_i : ι) => f j) = s.prod fun (i : ι) => f (g i)

theorem Finset.sum_fiberwise {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : ι → α) : (Finset.univ.sum fun (j : κ) => (Finset.filter (fun (i : ι) => g i = j) s).sum fun (i : ι) => f i) = s.sum fun (i : ι) => f i

theorem Finset.prod_fiberwise {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : ι → α) : (Finset.univ.prod fun (j : κ) => (Finset.filter (fun (i : ι) => g i = j) s).prod fun (i : ι) => f i) = s.prod fun (i : ι) => f i

theorem Finset.sum_fiberwise' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : κ → α) : (Finset.univ.sum fun (j : κ) => (Finset.filter (fun (i : ι) => g i = j) s).sum fun (_i : ι) => f j) = s.sum fun (i : ι) => f (g i)

theorem Finset.prod_fiberwise' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : κ → α) : (Finset.univ.prod fun (j : κ) => (Finset.filter (fun (i : ι) => g i = j) s).prod fun (_i : ι) => f j) = s.prod fun (i : ι) => f (g i)

theorem Finset.sum_univ_pi {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] [DecidableEq ι] [Fintype ι] {κ : ι → Type u_6} (t : (i : ι) → Finset (κ i)) (f : ((i : ι) → i ∈ Finset.univ → κ i) → β) : ((Finset.univ.pi t).sum fun (x : (a : ι) → a ∈ Finset.univ → κ a) => f x) = (Fintype.piFinset t).sum fun (x : (a : ι) → κ a) => f fun (a : ι) (x_1 : a ∈ Finset.univ) => x a

Taking a sum over univ.pi t is the same as taking the sum over Fintype.piFinset t. univ.pi t and Fintype.piFinset t are essentially the same Finset, but differ in the type of their element, univ.pi t is a Finset (Π a ∈ univ, t a) and Fintype.piFinset t is a Finset (Π a, t a).

theorem Finset.prod_univ_pi {ι : Type u_1} {β : Type u_4} [CommMonoid β] [DecidableEq ι] [Fintype ι] {κ : ι → Type u_6} (t : (i : ι) → Finset (κ i)) (f : ((i : ι) → i ∈ Finset.univ → κ i) → β) : ((Finset.univ.pi t).prod fun (x : (a : ι) → a ∈ Finset.univ → κ a) => f x) = (Fintype.piFinset t).prod fun (x : (a : ι) → κ a) => f fun (a : ι) (x_1 : a ∈ Finset.univ) => x a

Taking a product over univ.pi t is the same as taking the product over Fintype.piFinset t. univ.pi t and Fintype.piFinset t are essentially the same Finset, but differ in the type of their element, univ.pi t is a Finset (Π a ∈ univ, t a) and Fintype.piFinset t is a Finset (Π a, t a).

@[simp]

theorem Finset.sum_diag {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (f : α × α → β) : (s.diag.sum fun (i : α × α) => f i) = s.sum fun (i : α) => f (i, i)

@[simp]

theorem Finset.prod_diag {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (f : α × α → β) : (s.diag.prod fun (i : α × α) => f i) = s.prod fun (i : α) => f (i, i)

theorem Finset.sum_finset_product {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ × α → β} : (r.sum fun (p : γ × α) => f p) = s.sum fun (c : γ) => (t c).sum fun (a : α) => f (c, a)

theorem Finset.prod_finset_product {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ × α → β} : (r.prod fun (p : γ × α) => f p) = s.prod fun (c : γ) => (t c).prod fun (a : α) => f (c, a)

theorem Finset.sum_finset_product' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ → α → β} : (r.sum fun (p : γ × α) => f p.1 p.2) = s.sum fun (c : γ) => (t c).sum fun (a : α) => f c a

theorem Finset.prod_finset_product' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ → α → β} : (r.prod fun (p : γ × α) => f p.1 p.2) = s.prod fun (c : γ) => (t c).prod fun (a : α) => f c a

theorem Finset.sum_finset_product_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α × γ → β} : (r.sum fun (p : α × γ) => f p) = s.sum fun (c : γ) => (t c).sum fun (a : α) => f (a, c)

theorem Finset.prod_finset_product_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α × γ → β} : (r.prod fun (p : α × γ) => f p) = s.prod fun (c : γ) => (t c).prod fun (a : α) => f (a, c)

theorem Finset.sum_finset_product_right' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α → γ → β} : (r.sum fun (p : α × γ) => f p.1 p.2) = s.sum fun (c : γ) => (t c).sum fun (a : α) => f a c

theorem Finset.prod_finset_product_right' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α → γ → β} : (r.prod fun (p : α × γ) => f p.1 p.2) = s.prod fun (c : γ) => (t c).prod fun (a : α) => f a c

abbrev Finset.sum_image'.match_1 {α : Type u_2} {γ : Type u_1} {s : Finset γ} {g : γ → α} (_x : α) (motive : (∃ a ∈ s, g a = _x) → Prop) : ∀ (x : ∃ a ∈ s, g a = _x), (∀ (c : γ) (hcs : c ∈ s) (hc : g c = _x), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem Finset.sum_image' {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β} [AddCommMonoid β] [DecidableEq α] {s : Finset γ} {g : γ → α} (h : γ → β) (eq : ∀ c ∈ s, f (g c) = (Finset.filter (fun (c' : γ) => g c' = g c) s).sum fun (x : γ) => h x) : ((Finset.image g s).sum fun (x : α) => f x) = s.sum fun (x : γ) => h x

theorem Finset.prod_image' {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β} [CommMonoid β] [DecidableEq α] {s : Finset γ} {g : γ → α} (h : γ → β) (eq : ∀ c ∈ s, f (g c) = (Finset.filter (fun (c' : γ) => g c' = g c) s).prod fun (x : γ) => h x) : ((Finset.image g s).prod fun (x : α) => f x) = s.prod fun (x : γ) => h x

theorem Finset.sum_add_distrib {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} {g : α → β} [AddCommMonoid β] : (s.sum fun (x : α) => f x + g x) = (s.sum fun (x : α) => f x) + s.sum fun (x : α) => g x

theorem Finset.prod_mul_distrib {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} {g : α → β} [CommMonoid β] : (s.prod fun (x : α) => f x * g x) = (s.prod fun (x : α) => f x) * s.prod fun (x : α) => g x

theorem Finset.sum_add_sum_comm {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] (f : α → β) (g : α → β) (h : α → β) (i : α → β) : ((s.sum fun (a : α) => f a + g a) + s.sum fun (a : α) => h a + i a) = (s.sum fun (a : α) => f a + h a) + s.sum fun (a : α) => g a + i a

theorem Finset.prod_mul_prod_comm {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] (f : α → β) (g : α → β) (h : α → β) (i : α → β) : ((s.prod fun (a : α) => f a * g a) * s.prod fun (a : α) => h a * i a) = (s.prod fun (a : α) => f a * h a) * s.prod fun (a : α) => g a * i a

theorem Finset.sum_product {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset γ} {t : Finset α} {f : γ × α → β} : ((s ×ˢ t).sum fun (x : γ × α) => f x) = s.sum fun (x : γ) => t.sum fun (y : α) => f (x, y)

theorem Finset.prod_product {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ × α → β} : ((s ×ˢ t).prod fun (x : γ × α) => f x) = s.prod fun (x : γ) => t.prod fun (y : α) => f (x, y)

theorem Finset.sum_product' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} : ((s ×ˢ t).sum fun (x : γ × α) => f x.1 x.2) = s.sum fun (x : γ) => t.sum fun (y : α) => f x y

An uncurried version of Finset.sum_product

theorem Finset.prod_product' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} : ((s ×ˢ t).prod fun (x : γ × α) => f x.1 x.2) = s.prod fun (x : γ) => t.prod fun (y : α) => f x y

An uncurried version of Finset.prod_product.

theorem Finset.sum_product_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset γ} {t : Finset α} {f : γ × α → β} : ((s ×ˢ t).sum fun (x : γ × α) => f x) = t.sum fun (y : α) => s.sum fun (x : γ) => f (x, y)

theorem Finset.prod_product_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ × α → β} : ((s ×ˢ t).prod fun (x : γ × α) => f x) = t.prod fun (y : α) => s.prod fun (x : γ) => f (x, y)

theorem Finset.sum_product_right' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} : ((s ×ˢ t).sum fun (x : γ × α) => f x.1 x.2) = t.sum fun (y : α) => s.sum fun (x : γ) => f x y

An uncurried version of Finset.sum_product_right

theorem Finset.prod_product_right' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} : ((s ×ˢ t).prod fun (x : γ × α) => f x.1 x.2) = t.prod fun (y : α) => s.prod fun (x : γ) => f x y

An uncurried version of Finset.prod_product_right.

theorem Finset.sum_comm' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset γ} {t : γ → Finset α} {t' : Finset α} {s' : α → Finset γ} (h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') {f : γ → α → β} : (s.sum fun (x : γ) => (t x).sum fun (y : α) => f x y) = t'.sum fun (y : α) => (s' y).sum fun (x : γ) => f x y

Generalization of Finset.sum_comm to the case when the inner Finsets depend on the outer variable.

abbrev Finset.sum_comm'.match_1 {α : Type u_2} {γ : Type u_1} (motive : γ × α → Prop) : ∀ (x : γ × α), (∀ (x : γ) (y : α), motive (x, y)) → motive x

Equations

• ⋯ = ⋯

theorem Finset.prod_comm' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset γ} {t : γ → Finset α} {t' : Finset α} {s' : α → Finset γ} (h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') {f : γ → α → β} : (s.prod fun (x : γ) => (t x).prod fun (y : α) => f x y) = t'.prod fun (y : α) => (s' y).prod fun (x : γ) => f x y

Generalization of Finset.prod_comm to the case when the inner Finsets depend on the outer variable.

theorem Finset.sum_comm {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} : (s.sum fun (x : γ) => t.sum fun (y : α) => f x y) = t.sum fun (y : α) => s.sum fun (x : γ) => f x y

theorem Finset.prod_comm {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} : (s.prod fun (x : γ) => t.prod fun (y : α) => f x y) = t.prod fun (y : α) => s.prod fun (x : γ) => f x y

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 (s.sum fun (x : α) => f x) (s.sum fun (x : α) => g x)

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 (s.prod fun (x : α) => f x) (s.prod fun (x : α) => g x)

theorem Finset.sum_filter_of_ne {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] {p : α → Prop} [DecidablePred p] (hp : ∀ x ∈ s, f x ≠ 0 → p x) : ((Finset.filter p s).sum fun (x : α) => f x) = s.sum fun (x : α) => f x

theorem Finset.prod_filter_of_ne {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] {p : α → Prop} [DecidablePred p] (hp : ∀ x ∈ s, f x ≠ 1 → p x) : ((Finset.filter p s).prod fun (x : α) => f x) = s.prod fun (x : α) => f x

theorem Finset.sum_filter_ne_zero {α : Type u_3} {β : Type u_4} {f : α → β} [AddCommMonoid β] (s : Finset α) [(x : α) → Decidable (f x ≠ 0)] : ((Finset.filter (fun (x : α) => f x ≠ 0) s).sum fun (x : α) => f x) = s.sum fun (x : α) => f x

theorem Finset.prod_filter_ne_one {α : Type u_3} {β : Type u_4} {f : α → β} [CommMonoid β] (s : Finset α) [(x : α) → Decidable (f x ≠ 1)] : ((Finset.filter (fun (x : α) => f x ≠ 1) s).prod fun (x : α) => f x) = s.prod fun (x : α) => f x

theorem Finset.sum_filter {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] (p : α → Prop) [DecidablePred p] (f : α → β) : ((Finset.filter p s).sum fun (a : α) => f a) = s.sum fun (a : α) => if p a then f a else 0

theorem Finset.prod_filter {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] (p : α → Prop) [DecidablePred p] (f : α → β) : ((Finset.filter p s).prod fun (a : α) => f a) = s.prod fun (a : α) => if p a then f a else 1

theorem Finset.sum_eq_single_of_mem {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {f : α → β} (a : α) (h : a ∈ s) (h₀ : ∀ b ∈ s, b ≠ a → f b = 0) : (s.sum fun (x : α) => f x) = f a

theorem Finset.prod_eq_single_of_mem {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {f : α → β} (a : α) (h : a ∈ s) (h₀ : ∀ b ∈ s, b ≠ a → f b = 1) : (s.prod fun (x : α) => f x) = f a

theorem Finset.sum_eq_single {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {f : α → β} (a : α) (h₀ : ∀ b ∈ s, b ≠ a → f b = 0) (h₁ : a ∉ s → f a = 0) : (s.sum fun (x : α) => f x) = f a

theorem Finset.prod_eq_single {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {f : α → β} (a : α) (h₀ : ∀ b ∈ s, b ≠ a → f b = 1) (h₁ : a ∉ s → f a = 1) : (s.prod fun (x : α) => f x) = f a

theorem Finset.sum_union_eq_left {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [AddCommMonoid β] [DecidableEq α] (hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 0) : ((s₁ ∪ s₂).sum fun (a : α) => f a) = s₁.sum fun (a : α) => f a

theorem Finset.prod_union_eq_left {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [CommMonoid β] [DecidableEq α] (hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 1) : ((s₁ ∪ s₂).prod fun (a : α) => f a) = s₁.prod fun (a : α) => f a

theorem Finset.sum_union_eq_right {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [AddCommMonoid β] [DecidableEq α] (hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 0) : ((s₁ ∪ s₂).sum fun (a : α) => f a) = s₂.sum fun (a : α) => f a

theorem Finset.prod_union_eq_right {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [CommMonoid β] [DecidableEq α] (hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1) : ((s₁ ∪ s₂).prod fun (a : α) => f a) = s₂.prod fun (a : α) => f a

theorem Finset.sum_eq_add_of_mem {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {f : α → β} (a : α) (b : α) (ha : a ∈ s) (hb : b ∈ s) (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 0) : (s.sum fun (x : α) => f x) = f a + f b

theorem Finset.prod_eq_mul_of_mem {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {f : α → β} (a : α) (b : α) (ha : a ∈ s) (hb : b ∈ s) (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) : (s.prod fun (x : α) => f x) = f a * f b

theorem Finset.sum_eq_add {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {f : α → β} (a : α) (b : α) (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 0) (ha : a ∉ s → f a = 0) (hb : b ∉ s → f b = 0) : (s.sum fun (x : α) => f x) = f a + f b

theorem Finset.prod_eq_mul {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {f : α → β} (a : α) (b : α) (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) (ha : a ∉ s → f a = 1) (hb : b ∉ s → f b = 1) : (s.prod fun (x : α) => f x) = f a * f b

@[simp]

theorem Finset.sum_subtype_eq_sum_filter {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] (f : α → β) {p : α → Prop} [DecidablePred p] : ((Finset.subtype p s).sum fun (x : Subtype p) => f ↑x) = (Finset.filter p s).sum fun (x : α) => f x

A sum over s.subtype p equals one over s.filter p.

@[simp]

theorem Finset.prod_subtype_eq_prod_filter {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] (f : α → β) {p : α → Prop} [DecidablePred p] : ((Finset.subtype p s).prod fun (x : Subtype p) => f ↑x) = (Finset.filter p s).prod fun (x : α) => f x

A product over s.subtype p equals one over s.filter p.

theorem Finset.sum_subtype_of_mem {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] (f : α → β) {p : α → Prop} [DecidablePred p] (h : ∀ x ∈ s, p x) : ((Finset.subtype p s).sum fun (x : Subtype p) => f ↑x) = s.sum fun (x : α) => f x

If all elements of a Finset satisfy the predicate p, a sum over s.subtype p equals that sum over s.

theorem Finset.prod_subtype_of_mem {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] (f : α → β) {p : α → Prop} [DecidablePred p] (h : ∀ x ∈ s, p x) : ((Finset.subtype p s).prod fun (x : Subtype p) => f ↑x) = s.prod fun (x : α) => f x

If all elements of a Finset satisfy the predicate p, a product over s.subtype p equals that product over s.

theorem Finset.sum_subtype_map_embedding {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {p : α → Prop} {s : Finset { x : α // p x }} {f : { x : α // p x } → β} {g : α → β} (h : ∀ x ∈ s, g ↑x = f x) : ((Finset.map (Function.Embedding.subtype fun (x : α) => p x) s).sum fun (x : α) => g x) = s.sum fun (x : { x : α // p x }) => f x

A sum of a function over a Finset in a subtype equals a sum in the main type of a function that agrees with the first function on that Finset.

theorem Finset.prod_subtype_map_embedding {α : Type u_3} {β : Type u_4} [CommMonoid β] {p : α → Prop} {s : Finset { x : α // p x }} {f : { x : α // p x } → β} {g : α → β} (h : ∀ x ∈ s, g ↑x = f x) : ((Finset.map (Function.Embedding.subtype fun (x : α) => p x) s).prod fun (x : α) => g x) = s.prod fun (x : { x : α // p x }) => f x

A product of a function over a Finset in a subtype equals a product in the main type of a function that agrees with the first function on that Finset.

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

theorem Finset.prod_coe_sort_eq_attach {α : Type u_3} {β : Type u_4} (s : Finset α) [CommMonoid β] (f : { x : α // x ∈ s } → β) : (Finset.univ.prod fun (i : { x : α // x ∈ s }) => f i) = s.attach.prod fun (i : { x : α // x ∈ s }) => f i

theorem Finset.sum_coe_sort {α : Type u_3} {β : Type u_4} (s : Finset α) (f : α → β) [AddCommMonoid β] : (Finset.univ.sum fun (i : { x : α // x ∈ s }) => f ↑i) = s.sum fun (i : α) => f i

theorem Finset.prod_coe_sort {α : Type u_3} {β : Type u_4} (s : Finset α) (f : α → β) [CommMonoid β] : (Finset.univ.prod fun (i : { x : α // x ∈ s }) => f ↑i) = s.prod fun (i : α) => f i

theorem Finset.sum_finset_coe {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (f : α → β) (s : Finset α) : (Finset.univ.sum fun (i : ↑↑s) => f ↑i) = s.sum fun (i : α) => f i

theorem Finset.prod_finset_coe {α : Type u_3} {β : Type u_4} [CommMonoid β] (f : α → β) (s : Finset α) : (Finset.univ.prod fun (i : ↑↑s) => f ↑i) = s.prod fun (i : α) => f i

theorem Finset.sum_subtype {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {p : α → Prop} {F : Fintype (Subtype p)} (s : Finset α) (h : ∀ (x : α), x ∈ s ↔ p x) (f : α → β) : (s.sum fun (a : α) => f a) = Finset.univ.sum fun (a : Subtype p) => f ↑a

theorem Finset.prod_subtype {α : Type u_3} {β : Type u_4} [CommMonoid β] {p : α → Prop} {F : Fintype (Subtype p)} (s : Finset α) (h : ∀ (x : α), x ∈ s ↔ p x) (f : α → β) : (s.prod fun (a : α) => f a) = Finset.univ.prod fun (a : Subtype p) => f ↑a

theorem Finset.sum_preimage' {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [AddCommMonoid β] (f : ι → κ) [DecidablePred fun (x : κ) => x ∈ Set.range f] (s : Finset κ) (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β) : ((s.preimage f hf).sum fun (x : ι) => g (f x)) = (Finset.filter (fun (x : κ) => x ∈ Set.range f) s).sum fun (x : κ) => g x

theorem Finset.prod_preimage' {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [CommMonoid β] (f : ι → κ) [DecidablePred fun (x : κ) => x ∈ Set.range f] (s : Finset κ) (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β) : ((s.preimage f hf).prod fun (x : ι) => g (f x)) = (Finset.filter (fun (x : κ) => x ∈ Set.range f) s).prod fun (x : κ) => g x

theorem Finset.sum_preimage {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [AddCommMonoid β] (f : ι → κ) (s : Finset κ) (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β) (hg : ∀ x ∈ s, x ∉ Set.range f → g x = 0) : ((s.preimage f hf).sum fun (x : ι) => g (f x)) = s.sum fun (x : κ) => g x

theorem Finset.prod_preimage {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [CommMonoid β] (f : ι → κ) (s : Finset κ) (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β) (hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1) : ((s.preimage f hf).prod fun (x : ι) => g (f x)) = s.prod fun (x : κ) => g x

theorem Finset.sum_preimage_of_bij {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [AddCommMonoid β] (f : ι → κ) (s : Finset κ) (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) (g : κ → β) : ((s.preimage f ⋯).sum fun (x : ι) => g (f x)) = s.sum fun (x : κ) => g x

theorem Finset.prod_preimage_of_bij {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [CommMonoid β] (f : ι → κ) (s : Finset κ) (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) (g : κ → β) : ((s.preimage f ⋯).prod fun (x : ι) => g (f x)) = s.prod fun (x : κ) => g x

theorem Finset.sum_set_coe {α : Type u_3} {β : Type u_4} {f : α → β} [AddCommMonoid β] (s : Set α) [Fintype ↑s] : (Finset.univ.sum fun (i : ↑s) => f ↑i) = s.toFinset.sum fun (i : α) => f i

theorem Finset.prod_set_coe {α : Type u_3} {β : Type u_4} {f : α → β} [CommMonoid β] (s : Set α) [Fintype ↑s] : (Finset.univ.prod fun (i : ↑s) => f ↑i) = s.toFinset.prod fun (i : α) => f i

theorem Finset.sum_congr_set {α : Type u_6} [AddCommMonoid α] {β : Type u_7} [Fintype β] (s : Set β) [DecidablePred fun (x : β) => x ∈ s] (f : β → α) (g : ↑s → α) (w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩) (w' : ∀ x ∉ s, f x = 0) : Finset.univ.sum f = Finset.univ.sum g

The sum of a function g defined only on a set s is equal to the sum of a function f defined everywhere, as long as f and g agree on s, and f = 0 off s.

abbrev Finset.sum_congr_set.match_1 {β : Type u_1} [Fintype β] (s : Set β) [DecidablePred fun (x : β) => x ∈ s] (motive : (x : { x : β // x ∈ s }) → x ∈ Finset.univ → Prop) : ∀ (x : { x : β // x ∈ s }) (x_1 : x ∈ Finset.univ), (∀ (x : β) (h : x ∈ s) (x_2 : ⟨x, h⟩ ∈ Finset.univ), motive ⟨x, h⟩ x_2) → motive x x_1

Equations

• ⋯ = ⋯

theorem Finset.prod_congr_set {α : Type u_6} [CommMonoid α] {β : Type u_7} [Fintype β] (s : Set β) [DecidablePred fun (x : β) => x ∈ s] (f : β → α) (g : ↑s → α) (w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩) (w' : ∀ x ∉ s, f x = 1) : Finset.univ.prod f = Finset.univ.prod g

The product of a function g defined only on a set s is equal to the product of a function f defined everywhere, as long as f and g agree on s, and f = 1 off s.

theorem Finset.sum_apply_dite {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} [DecidablePred fun (x : α) => ¬p x] (f : (x : α) → p x → γ) (g : (x : α) → ¬p x → γ) (h : γ → β) : (s.sum fun (x : α) => h (if hx : p x then f x hx else g x hx)) = ((Finset.filter p s).attach.sum fun (x : { x : α // x ∈ Finset.filter p s }) => h (f ↑x ⋯)) + (Finset.filter (fun (x : α) => ¬p x) s).attach.sum fun (x : { x : α // x ∈ Finset.filter (fun (x : α) => ¬p x) s }) => h (g ↑x ⋯)

theorem Finset.prod_apply_dite {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} [DecidablePred fun (x : α) => ¬p x] (f : (x : α) → p x → γ) (g : (x : α) → ¬p x → γ) (h : γ → β) : (s.prod fun (x : α) => h (if hx : p x then f x hx else g x hx)) = ((Finset.filter p s).attach.prod fun (x : { x : α // x ∈ Finset.filter p s }) => h (f ↑x ⋯)) * (Finset.filter (fun (x : α) => ¬p x) s).attach.prod fun (x : { x : α // x ∈ Finset.filter (fun (x : α) => ¬p x) s }) => h (g ↑x ⋯)

theorem Finset.sum_apply_ite {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset α} {p : α → Prop} {_hp : DecidablePred p} (f : α → γ) (g : α → γ) (h : γ → β) : (s.sum fun (x : α) => h (if p x then f x else g x)) = ((Finset.filter p s).sum fun (x : α) => h (f x)) + (Finset.filter (fun (x : α) => ¬p x) s).sum fun (x : α) => h (g x)

theorem Finset.prod_apply_ite {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset α} {p : α → Prop} {_hp : DecidablePred p} (f : α → γ) (g : α → γ) (h : γ → β) : (s.prod fun (x : α) => h (if p x then f x else g x)) = ((Finset.filter p s).prod fun (x : α) => h (f x)) * (Finset.filter (fun (x : α) => ¬p x) s).prod fun (x : α) => h (g x)

theorem Finset.sum_dite {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (s.sum fun (x : α) => if hx : p x then f x hx else g x hx) = ((Finset.filter p s).attach.sum fun (x : { x : α // x ∈ Finset.filter p s }) => f ↑x ⋯) + (Finset.filter (fun (x : α) => ¬p x) s).attach.sum fun (x : { x : α // x ∈ Finset.filter (fun (x : α) => ¬p x) s }) => g ↑x ⋯

theorem Finset.prod_dite {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (s.prod fun (x : α) => if hx : p x then f x hx else g x hx) = ((Finset.filter p s).attach.prod fun (x : { x : α // x ∈ Finset.filter p s }) => f ↑x ⋯) * (Finset.filter (fun (x : α) => ¬p x) s).attach.prod fun (x : { x : α // x ∈ Finset.filter (fun (x : α) => ¬p x) s }) => g ↑x ⋯

theorem Finset.sum_ite {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : α → β) (g : α → β) : (s.sum fun (x : α) => if p x then f x else g x) = ((Finset.filter p s).sum fun (x : α) => f x) + (Finset.filter (fun (x : α) => ¬p x) s).sum fun (x : α) => g x

theorem Finset.prod_ite {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : α → β) (g : α → β) : (s.prod fun (x : α) => if p x then f x else g x) = ((Finset.filter p s).prod fun (x : α) => f x) * (Finset.filter (fun (x : α) => ¬p x) s).prod fun (x : α) => g x

theorem Finset.sum_ite_of_false {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → β) (g : α → β) (h : ∀ x ∈ s, ¬p x) : (s.sum fun (x : α) => if p x then f x else g x) = s.sum fun (x : α) => g x

theorem Finset.prod_ite_of_false {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → β) (g : α → β) (h : ∀ x ∈ s, ¬p x) : (s.prod fun (x : α) => if p x then f x else g x) = s.prod fun (x : α) => g x

theorem Finset.sum_ite_of_true {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → β) (g : α → β) (h : ∀ x ∈ s, p x) : (s.sum fun (x : α) => if p x then f x else g x) = s.sum fun (x : α) => f x

theorem Finset.prod_ite_of_true {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → β) (g : α → β) (h : ∀ x ∈ s, p x) : (s.prod fun (x : α) => if p x then f x else g x) = s.prod fun (x : α) => f x

theorem Finset.sum_apply_ite_of_false {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → γ) (g : α → γ) (k : γ → β) (h : ∀ x ∈ s, ¬p x) : (s.sum fun (x : α) => k (if p x then f x else g x)) = s.sum fun (x : α) => k (g x)

theorem Finset.prod_apply_ite_of_false {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → γ) (g : α → γ) (k : γ → β) (h : ∀ x ∈ s, ¬p x) : (s.prod fun (x : α) => k (if p x then f x else g x)) = s.prod fun (x : α) => k (g x)

theorem Finset.sum_apply_ite_of_true {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → γ) (g : α → γ) (k : γ → β) (h : ∀ x ∈ s, p x) : (s.sum fun (x : α) => k (if p x then f x else g x)) = s.sum fun (x : α) => k (f x)

theorem Finset.prod_apply_ite_of_true {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → γ) (g : α → γ) (k : γ → β) (h : ∀ x ∈ s, p x) : (s.prod fun (x : α) => k (if p x then f x else g x)) = s.prod fun (x : α) => k (f x)

theorem Finset.sum_extend_by_zero {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) : (s.sum fun (i : α) => if i ∈ s then f i else 0) = s.sum fun (i : α) => f i

theorem Finset.prod_extend_by_one {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) : (s.prod fun (i : α) => if i ∈ s then f i else 1) = s.prod fun (i : α) => f i

@[simp]

theorem Finset.sum_ite_mem {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (t : Finset α) (f : α → β) : (s.sum fun (i : α) => if i ∈ t then f i else 0) = (s ∩ t).sum fun (i : α) => f i

@[simp]

theorem Finset.prod_ite_mem {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (t : Finset α) (f : α → β) : (s.prod fun (i : α) => if i ∈ t then f i else 1) = (s ∩ t).prod fun (i : α) => f i

@[simp]

theorem Finset.sum_dite_eq {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → a = x → β) : (s.sum fun (x : α) => if h : a = x then b x h else 0) = if a ∈ s then b a ⋯ else 0

@[simp]

theorem Finset.prod_dite_eq {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → a = x → β) : (s.prod fun (x : α) => if h : a = x then b x h else 1) = if a ∈ s then b a ⋯ else 1

@[simp]

theorem Finset.sum_dite_eq' {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → x = a → β) : (s.sum fun (x : α) => if h : x = a then b x h else 0) = if a ∈ s then b a ⋯ else 0

@[simp]

theorem Finset.prod_dite_eq' {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → x = a → β) : (s.prod fun (x : α) => if h : x = a then b x h else 1) = if a ∈ s then b a ⋯ else 1

@[simp]

theorem Finset.sum_ite_eq {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (s.sum fun (x : α) => if a = x then b x else 0) = if a ∈ s then b a else 0

@[simp]

theorem Finset.prod_ite_eq {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (s.prod fun (x : α) => if a = x then b x else 1) = if a ∈ s then b a else 1

@[simp]

theorem Finset.sum_ite_eq' {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (s.sum fun (x : α) => if x = a then b x else 0) = if a ∈ s then b a else 0

A sum taken over a conditional whose condition is an equality test on the index and whose alternative is 0 has value either the term at that index or 0.

The difference with Finset.sum_ite_eq is that the arguments to Eq are swapped.

@[simp]

theorem Finset.prod_ite_eq' {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (s.prod fun (x : α) => if x = a then b x else 1) = if a ∈ s then b a else 1

A product taken over a conditional whose condition is an equality test on the index and whose alternative is 1 has value either the term at that index or 1.

The difference with Finset.prod_ite_eq is that the arguments to Eq are swapped.

theorem Finset.sum_ite_index {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (t : Finset α) (f : α → β) : ((if p then s else t).sum fun (x : α) => f x) = if p then s.sum fun (x : α) => f x else t.sum fun (x : α) => f x

theorem Finset.prod_ite_index {α : Type u_3} {β : Type u_4} [CommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (t : Finset α) (f : α → β) : ((if p then s else t).prod fun (x : α) => f x) = if p then s.prod fun (x : α) => f x else t.prod fun (x : α) => f x

@[simp]

theorem Finset.sum_ite_irrel {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f : α → β) (g : α → β) : (s.sum fun (x : α) => if p then f x else g x) = if p then s.sum fun (x : α) => f x else s.sum fun (x : α) => g x

@[simp]

theorem Finset.prod_ite_irrel {α : Type u_3} {β : Type u_4} [CommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f : α → β) (g : α → β) : (s.prod fun (x : α) => if p then f x else g x) = if p then s.prod fun (x : α) => f x else s.prod fun (x : α) => g x

@[simp]

theorem Finset.sum_dite_irrel {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f : p → α → β) (g : ¬p → α → β) : (s.sum fun (x : α) => if h : p then f h x else g h x) = if h : p then s.sum fun (x : α) => f h x else s.sum fun (x : α) => g h x

@[simp]

theorem Finset.prod_dite_irrel {α : Type u_3} {β : Type u_4} [CommMonoid β] (p : Prop) [Decidable p] (s : Finset α) (f : p → α → β) (g : ¬p → α → β) : (s.prod fun (x : α) => if h : p then f h x else g h x) = if h : p then s.prod fun (x : α) => f h x else s.prod fun (x : α) => g h x

@[simp]

theorem Finset.sum_pi_single' {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (a : α) (x : β) (s : Finset α) : (s.sum fun (a' : α) => Pi.single a x a') = if a ∈ s then x else 0

@[simp]

theorem Finset.prod_pi_mulSingle' {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (a : α) (x : β) (s : Finset α) : (s.prod fun (a' : α) => Pi.mulSingle a x a') = if a ∈ s then x else 1

@[simp]

theorem Finset.sum_pi_single {α : Type u_3} {β : α → Type u_6} [DecidableEq α] [(a : α) → AddCommMonoid (β a)] (a : α) (f : (a : α) → β a) (s : Finset α) : (s.sum fun (a' : α) => Pi.single a' (f a') a) = if a ∈ s then f a else 0

@[simp]

theorem Finset.prod_pi_mulSingle {α : Type u_3} {β : α → Type u_6} [DecidableEq α] [(a : α) → CommMonoid (β a)] (a : α) (f : (a : α) → β a) (s : Finset α) : (s.prod fun (a' : α) => Pi.mulSingle a' (f a') a) = if a ∈ s then f a else 1

theorem Finset.support_sum {ι : Type u_1} {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset ι) (f : ι → α → β) : (Function.support fun (x : α) => s.sum fun (i : ι) => f i x) ⊆ ⋃ i ∈ s, Function.support (f i)

theorem Finset.mulSupport_prod {ι : Type u_1} {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset ι) (f : ι → α → β) : (Function.mulSupport fun (x : α) => s.prod fun (i : ι) => f i x) ⊆ ⋃ i ∈ s, Function.mulSupport (f i)

theorem Finset.sum_indicator_subset_of_eq_zero {ι : Type u_1} {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [Zero α] (f : ι → α) (g : ι → α → β) {s : Finset ι} {t : Finset ι} (h : s ⊆ t) (hg : ∀ (a : ι), g a 0 = 0) : (t.sum fun (i : ι) => g i ((↑s).indicator f i)) = s.sum fun (i : ι) => g i (f i)

Consider a sum of g i (f i) over a finset. Suppose g is a function such as n ↦ (n • ·), which maps a second argument of 0 to 0 (or a weighted sum of f i * h i or f i • h i, where f gives the weights that are multiplied by some other function h). Then if f is replaced by the corresponding indicator function, the finset may be replaced by a possibly larger finset without changing the value of the sum.

theorem Finset.prod_mulIndicator_subset_of_eq_one {ι : Type u_1} {α : Type u_3} {β : Type u_4} [CommMonoid β] [One α] (f : ι → α) (g : ι → α → β) {s : Finset ι} {t : Finset ι} (h : s ⊆ t) (hg : ∀ (a : ι), g a 1 = 1) : (t.prod fun (i : ι) => g i ((↑s).mulIndicator f i)) = s.prod fun (i : ι) => g i (f i)

Consider a product of g i (f i) over a finset. Suppose g is a function such as n ↦ (· ^ n), which maps a second argument of 1 to 1. Then if f is replaced by the corresponding multiplicative indicator function, the finset may be replaced by a possibly larger finset without changing the value of the product.

theorem Finset.sum_indicator_subset {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] (f : ι → β) {s : Finset ι} {t : Finset ι} (h : s ⊆ t) : (t.sum fun (i : ι) => (↑s).indicator f i) = s.sum fun (i : ι) => f i

Summing an indicator function over a possibly larger Finset is the same as summing the original function over the original finset.

theorem Finset.prod_mulIndicator_subset {ι : Type u_1} {β : Type u_4} [CommMonoid β] (f : ι → β) {s : Finset ι} {t : Finset ι} (h : s ⊆ t) : (t.prod fun (i : ι) => (↑s).mulIndicator f i) = s.prod fun (i : ι) => f i

Taking the product of an indicator function over a possibly larger finset is the same as taking the original function over the original finset.

theorem Finset.sum_indicator_eq_sum_filter {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] {κ : Type u_6} (s : Finset ι) (f : ι → κ → β) (t : ι → Set κ) (g : ι → κ) [DecidablePred fun (i : ι) => g i ∈ t i] : (s.sum fun (i : ι) => (t i).indicator (f i) (g i)) = (Finset.filter (fun (i : ι) => g i ∈ t i) s).sum fun (i : ι) => f i (g i)

theorem Finset.prod_mulIndicator_eq_prod_filter {ι : Type u_1} {β : Type u_4} [CommMonoid β] {κ : Type u_6} (s : Finset ι) (f : ι → κ → β) (t : ι → Set κ) (g : ι → κ) [DecidablePred fun (i : ι) => g i ∈ t i] : (s.prod fun (i : ι) => (t i).mulIndicator (f i) (g i)) = (Finset.filter (fun (i : ι) => g i ∈ t i) s).prod fun (i : ι) => f i (g i)

theorem Finset.sum_indicator_eq_sum_inter {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] [DecidableEq ι] (s : Finset ι) (t : Finset ι) (f : ι → β) : (s.sum fun (i : ι) => (↑t).indicator f i) = (s ∩ t).sum fun (i : ι) => f i

theorem Finset.prod_mulIndicator_eq_prod_inter {ι : Type u_1} {β : Type u_4} [CommMonoid β] [DecidableEq ι] (s : Finset ι) (t : Finset ι) (f : ι → β) : (s.prod fun (i : ι) => (↑t).mulIndicator f i) = (s ∩ t).prod fun (i : ι) => f i

theorem Finset.indicator_sum {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] {κ : Type u_6} (s : Finset ι) (t : Set κ) (f : ι → κ → β) : t.indicator (s.sum fun (i : ι) => f i) = s.sum fun (i : ι) => t.indicator (f i)

theorem Finset.mulIndicator_prod {ι : Type u_1} {β : Type u_4} [CommMonoid β] {κ : Type u_6} (s : Finset ι) (t : Set κ) (f : ι → κ → β) : t.mulIndicator (s.prod fun (i : ι) => f i) = s.prod fun (i : ι) => t.mulIndicator (f i)

theorem Finset.indicator_biUnion {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] {κ : Type u_7} (s : Finset ι) (t : ι → Set κ) {f : κ → β} : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).indicator f = fun (a : κ) => s.sum fun (i : ι) => (t i).indicator f a

theorem Finset.mulIndicator_biUnion {ι : Type u_1} {β : Type u_4} [CommMonoid β] {κ : Type u_7} (s : Finset ι) (t : ι → Set κ) {f : κ → β} : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun (a : κ) => s.prod fun (i : ι) => (t i).mulIndicator f a

theorem Finset.indicator_biUnion_apply {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] {κ : Type u_7} (s : Finset ι) (t : ι → Set κ) {f : κ → β} (h : (↑s).PairwiseDisjoint t) (x : κ) : (⋃ i ∈ s, t i).indicator f x = s.sum fun (i : ι) => (t i).indicator f x

theorem Finset.mulIndicator_biUnion_apply {ι : Type u_1} {β : Type u_4} [CommMonoid β] {κ : Type u_7} (s : Finset ι) (t : ι → Set κ) {f : κ → β} (h : (↑s).PairwiseDisjoint t) (x : κ) : (⋃ i ∈ s, t i).mulIndicator f x = s.prod fun (i : ι) => (t i).mulIndicator f x

theorem Finset.sum_bij_ne_zero {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β} (i : (a : α) → a ∈ s → f a ≠ 0 → γ) (hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), i a h₁ h₂ ∈ t) (i_inj : ∀ (a₁ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 0) (a₂ : α) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 0), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, g b ≠ 0 → ∃ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), i a h₁ h₂ = b) (h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), f a = g (i a h₁ h₂)) : (s.sum fun (x : α) => f x) = t.sum fun (x : γ) => g x

theorem Finset.prod_bij_ne_one {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β} (i : (a : α) → a ∈ s → f a ≠ 1 → γ) (hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t) (i_inj : ∀ (a₁ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : α) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b) (h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)) : (s.prod fun (x : α) => f x) = t.prod fun (x : γ) => g x

theorem Finset.sum_dite_of_false {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (h : ∀ x ∈ s, ¬p x) (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (s.sum fun (x : α) => if hx : p x then f x hx else g x hx) = Finset.univ.sum fun (x : { x : α // x ∈ s }) => g ↑x ⋯

theorem Finset.prod_dite_of_false {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (h : ∀ x ∈ s, ¬p x) (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (s.prod fun (x : α) => if hx : p x then f x hx else g x hx) = Finset.univ.prod fun (x : { x : α // x ∈ s }) => g ↑x ⋯

theorem Finset.sum_dite_of_true {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (h : ∀ x ∈ s, p x) (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (s.sum fun (x : α) => if hx : p x then f x hx else g x hx) = Finset.univ.sum fun (x : { x : α // x ∈ s }) => f ↑x ⋯

theorem Finset.prod_dite_of_true {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (h : ∀ x ∈ s, p x) (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (s.prod fun (x : α) => if hx : p x then f x hx else g x hx) = Finset.univ.prod fun (x : { x : α // x ∈ s }) => f ↑x ⋯

theorem Finset.nonempty_of_sum_ne_zero {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] (h : (s.sum fun (x : α) => f x) ≠ 0) : s.Nonempty

theorem Finset.nonempty_of_prod_ne_one {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] (h : (s.prod fun (x : α) => f x) ≠ 1) : s.Nonempty

theorem Finset.exists_ne_zero_of_sum_ne_zero {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] (h : (s.sum fun (x : α) => f x) ≠ 0) : ∃ a ∈ s, f a ≠ 0

theorem Finset.exists_ne_one_of_prod_ne_one {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] (h : (s.prod fun (x : α) => f x) ≠ 1) : ∃ a ∈ s, f a ≠ 1

theorem Finset.sum_range_succ_comm {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) (n : ℕ) : ((Finset.range (n + 1)).sum fun (x : ℕ) => f x) = f n + (Finset.range n).sum fun (x : ℕ) => f x

theorem Finset.prod_range_succ_comm {β : Type u_4} [CommMonoid β] (f : ℕ → β) (n : ℕ) : ((Finset.range (n + 1)).prod fun (x : ℕ) => f x) = f n * (Finset.range n).prod fun (x : ℕ) => f x

theorem Finset.sum_range_succ {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) (n : ℕ) : ((Finset.range (n + 1)).sum fun (x : ℕ) => f x) = ((Finset.range n).sum fun (x : ℕ) => f x) + f n

theorem Finset.prod_range_succ {β : Type u_4} [CommMonoid β] (f : ℕ → β) (n : ℕ) : ((Finset.range (n + 1)).prod fun (x : ℕ) => f x) = ((Finset.range n).prod fun (x : ℕ) => f x) * f n

theorem Finset.sum_range_succ' {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) (n : ℕ) : ((Finset.range (n + 1)).sum fun (k : ℕ) => f k) = ((Finset.range n).sum fun (k : ℕ) => f (k + 1)) + f 0

abbrev Finset.sum_range_succ'.match_1 (motive : ℕ → Prop) : ∀ (x : ℕ), (Unit → motive 0) → (∀ (n : ℕ), motive n.succ) → motive x

Equations

• ⋯ = ⋯

theorem Finset.prod_range_succ' {β : Type u_4} [CommMonoid β] (f : ℕ → β) (n : ℕ) : ((Finset.range (n + 1)).prod fun (k : ℕ) => f k) = ((Finset.range n).prod fun (k : ℕ) => f (k + 1)) * f 0

theorem Finset.eventually_constant_sum {β : Type u_4} [AddCommMonoid β] {u : ℕ → β} {N : ℕ} (hu : ∀ n ≥ N, u n = 0) {n : ℕ} (hn : N ≤ n) : ((Finset.range n).sum fun (k : ℕ) => u k) = (Finset.range N).sum fun (k : ℕ) => u k

theorem Finset.eventually_constant_prod {β : Type u_4} [CommMonoid β] {u : ℕ → β} {N : ℕ} (hu : ∀ n ≥ N, u n = 1) {n : ℕ} (hn : N ≤ n) : ((Finset.range n).prod fun (k : ℕ) => u k) = (Finset.range N).prod fun (k : ℕ) => u k

theorem Finset.sum_range_add {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) (n : ℕ) (m : ℕ) : ((Finset.range (n + m)).sum fun (x : ℕ) => f x) = ((Finset.range n).sum fun (x : ℕ) => f x) + (Finset.range m).sum fun (x : ℕ) => f (n + x)

theorem Finset.prod_range_add {β : Type u_4} [CommMonoid β] (f : ℕ → β) (n : ℕ) (m : ℕ) : ((Finset.range (n + m)).prod fun (x : ℕ) => f x) = ((Finset.range n).prod fun (x : ℕ) => f x) * (Finset.range m).prod fun (x : ℕ) => f (n + x)

theorem Finset.sum_range_add_sub_sum_range {α : Type u_6} [AddCommGroup α] (f : ℕ → α) (n : ℕ) (m : ℕ) : (((Finset.range (n + m)).sum fun (k : ℕ) => f k) - (Finset.range n).sum fun (k : ℕ) => f k) = (Finset.range m).sum fun (k : ℕ) => f (n + k)

theorem Finset.prod_range_add_div_prod_range {α : Type u_6} [CommGroup α] (f : ℕ → α) (n : ℕ) (m : ℕ) : (((Finset.range (n + m)).prod fun (k : ℕ) => f k) / (Finset.range n).prod fun (k : ℕ) => f k) = (Finset.range m).prod fun (k : ℕ) => f (n + k)

theorem Finset.sum_range_zero {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) : ((Finset.range 0).sum fun (k : ℕ) => f k) = 0

theorem Finset.prod_range_zero {β : Type u_4} [CommMonoid β] (f : ℕ → β) : ((Finset.range 0).prod fun (k : ℕ) => f k) = 1

theorem Finset.sum_range_one {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) : ((Finset.range 1).sum fun (k : ℕ) => f k) = f 0

theorem Finset.prod_range_one {β : Type u_4} [CommMonoid β] (f : ℕ → β) : ((Finset.range 1).prod fun (k : ℕ) => f k) = f 0

theorem Finset.sum_list_map_count {α : Type u_3} [DecidableEq α] (l : List α) {M : Type u_6} [AddCommMonoid M] (f : α → M) : (List.map f l).sum = l.toFinset.sum fun (m : α) => List.count m l • f m

theorem Finset.prod_list_map_count {α : Type u_3} [DecidableEq α] (l : List α) {M : Type u_6} [CommMonoid M] (f : α → M) : (List.map f l).prod = l.toFinset.prod fun (m : α) => f m ^ List.count m l

theorem Finset.sum_list_count {α : Type u_3} [DecidableEq α] [AddCommMonoid α] (s : List α) : s.sum = s.toFinset.sum fun (m : α) => List.count m s • m

theorem Finset.prod_list_count {α : Type u_3} [DecidableEq α] [CommMonoid α] (s : List α) : s.prod = s.toFinset.prod fun (m : α) => m ^ List.count m s

theorem Finset.sum_list_count_of_subset {α : Type u_3} [DecidableEq α] [AddCommMonoid α] (m : List α) (s : Finset α) (hs : m.toFinset ⊆ s) : m.sum = s.sum fun (i : α) => List.count i m • i

theorem Finset.prod_list_count_of_subset {α : Type u_3} [DecidableEq α] [CommMonoid α] (m : List α) (s : Finset α) (hs : m.toFinset ⊆ s) : m.prod = s.prod fun (i : α) => i ^ List.count i m

theorem Finset.sum_filter_count_eq_countP {α : Type u_3} [DecidableEq α] (p : α → Prop) [DecidablePred p] (l : List α) : ((Finset.filter p l.toFinset).sum fun (x : α) => List.count x l) = List.countP (fun (b : α) => decide (p b)) l

theorem Finset.sum_multiset_map_count {α : Type u_3} [DecidableEq α] (s : Multiset α) {M : Type u_6} [AddCommMonoid M] (f : α → M) : (Multiset.map f s).sum = s.toFinset.sum fun (m : α) => Multiset.count m s • f m

theorem Finset.prod_multiset_map_count {α : Type u_3} [DecidableEq α] (s : Multiset α) {M : Type u_6} [CommMonoid M] (f : α → M) : (Multiset.map f s).prod = s.toFinset.prod fun (m : α) => f m ^ Multiset.count m s

theorem Finset.sum_multiset_count {α : Type u_3} [DecidableEq α] [AddCommMonoid α] (s : Multiset α) : s.sum = s.toFinset.sum fun (m : α) => Multiset.count m s • m

theorem Finset.prod_multiset_count {α : Type u_3} [DecidableEq α] [CommMonoid α] (s : Multiset α) : s.prod = s.toFinset.prod fun (m : α) => m ^ Multiset.count m s

theorem Finset.sum_multiset_count_of_subset {α : Type u_3} [DecidableEq α] [AddCommMonoid α] (m : Multiset α) (s : Finset α) (hs : m.toFinset ⊆ s) : m.sum = s.sum fun (i : α) => Multiset.count i m • i

theorem Finset.prod_multiset_count_of_subset {α : Type u_3} [DecidableEq α] [CommMonoid α] (m : Multiset α) (s : Finset α) (hs : m.toFinset ⊆ s) : m.prod = s.prod fun (i : α) => i ^ Multiset.count i m

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) : (Finset.univ.sum fun (x : { x : α // x ∈ m }) => f x) = m.toFinset.sum fun (x : α) => g x

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) : (Finset.univ.prod fun (x : { x : α // x ∈ m }) => f x) = m.toFinset.prod fun (x : α) => g x

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 (s.sum fun (x : α) => 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 {α : 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 (s.prod fun (x : α) => 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 (s.sum fun (x : α) => 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 (s.prod fun (x : α) => 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_range_induction {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) (s : ℕ → β) (base : s 0 = 0) (step : ∀ (n : ℕ), s (n + 1) = s n + f n) (n : ℕ) : ((Finset.range n).sum fun (k : ℕ) => f k) = s n

For any sum along {0, ..., n - 1} of a commutative-monoid-valued function, we can verify that it's equal to a different function just by checking differences of adjacent terms.

This is a discrete analogue of the fundamental theorem of calculus.

theorem Finset.prod_range_induction {β : Type u_4} [CommMonoid β] (f : ℕ → β) (s : ℕ → β) (base : s 0 = 1) (step : ∀ (n : ℕ), s (n + 1) = s n * f n) (n : ℕ) : ((Finset.range n).prod fun (k : ℕ) => f k) = s n

For any product along {0, ..., n - 1} of a commutative-monoid-valued function, we can verify that it's equal to a different function just by checking ratios of adjacent terms.

This is a multiplicative discrete analogue of the fundamental theorem of calculus.

theorem Finset.sum_range_sub {M : Type u_6} [AddCommGroup M] (f : ℕ → M) (n : ℕ) : ((Finset.range n).sum fun (i : ℕ) => f (i + 1) - f i) = f n - f 0

A telescoping sum along {0, ..., n - 1} of an additive commutative group valued function reduces to the difference of the last and first terms.

theorem Finset.prod_range_div {M : Type u_6} [CommGroup M] (f : ℕ → M) (n : ℕ) : ((Finset.range n).prod fun (i : ℕ) => f (i + 1) / f i) = f n / f 0

A telescoping product along {0, ..., n - 1} of a commutative group valued function reduces to the ratio of the last and first factors.

theorem Finset.sum_range_sub' {M : Type u_6} [AddCommGroup M] (f : ℕ → M) (n : ℕ) : ((Finset.range n).sum fun (i : ℕ) => f i - f (i + 1)) = f 0 - f n

theorem Finset.prod_range_div' {M : Type u_6} [CommGroup M] (f : ℕ → M) (n : ℕ) : ((Finset.range n).prod fun (i : ℕ) => f i / f (i + 1)) = f 0 / f n

theorem Finset.eq_sum_range_sub {M : Type u_6} [AddCommGroup M] (f : ℕ → M) (n : ℕ) : f n = f 0 + (Finset.range n).sum fun (i : ℕ) => f (i + 1) - f i

theorem Finset.eq_prod_range_div {M : Type u_6} [CommGroup M] (f : ℕ → M) (n : ℕ) : f n = f 0 * (Finset.range n).prod fun (i : ℕ) => f (i + 1) / f i

theorem Finset.eq_sum_range_sub' {M : Type u_6} [AddCommGroup M] (f : ℕ → M) (n : ℕ) : f n = (Finset.range (n + 1)).sum fun (i : ℕ) => if i = 0 then f 0 else f i - f (i - 1)

theorem Finset.eq_prod_range_div' {M : Type u_6} [CommGroup M] (f : ℕ → M) (n : ℕ) : f n = (Finset.range (n + 1)).prod fun (i : ℕ) => if i = 0 then f 0 else f i / f (i - 1)

theorem Finset.sum_range_tsub {α : Type u_3} [CanonicallyOrderedAddCommMonoid α] [Sub α] [OrderedSub α] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] {f : ℕ → α} (h : Monotone f) (n : ℕ) : ((Finset.range n).sum fun (i : ℕ) => f (i + 1) - f i) = f n - f 0

A telescoping sum along {0, ..., n-1} of an ℕ-valued function reduces to the difference of the last and first terms when the function we are summing is monotone.

@[simp]

theorem Finset.sum_const {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] (b : β) : (s.sum fun (_x : α) => b) = s.card • b

@[simp]

theorem Finset.prod_const {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] (b : β) : (s.prod fun (_x : α) => b) = b ^ s.card

theorem Finset.sum_eq_card_nsmul {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] {b : β} (hf : ∀ a ∈ s, f a = b) : (s.sum fun (a : α) => f a) = s.card • b

theorem Finset.prod_eq_pow_card {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] {b : β} (hf : ∀ a ∈ s, f a = b) : (s.prod fun (a : α) => f a) = b ^ s.card

theorem Finset.card_nsmul_add_sum {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] {b : β} : (s.card • b + s.sum fun (a : α) => f a) = s.sum fun (a : α) => b + f a

theorem Finset.pow_card_mul_prod {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] {b : β} : (b ^ s.card * s.prod fun (a : α) => f a) = s.prod fun (a : α) => b * f a

theorem Finset.sum_add_card_nsmul {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] {b : β} : (s.sum fun (a : α) => f a) + s.card • b = s.sum fun (a : α) => f a + b

theorem Finset.prod_mul_pow_card {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] {b : β} : (s.prod fun (a : α) => f a) * b ^ s.card = s.prod fun (a : α) => f a * b

theorem Finset.nsmul_eq_sum_const {β : Type u_4} [AddCommMonoid β] (b : β) (n : ℕ) : n • b = (Finset.range n).sum fun (_k : ℕ) => b

theorem Finset.pow_eq_prod_const {β : Type u_4} [CommMonoid β] (b : β) (n : ℕ) : b ^ n = (Finset.range n).prod fun (_k : ℕ) => b

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

theorem Finset.prod_pow {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (n : ℕ) (f : α → β) : (s.prod fun (x : α) => f x ^ n) = (s.prod fun (x : α) => f x) ^ n

theorem Finset.sum_nsmul_assoc {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] (s : Finset ι) (f : ι → ℕ) (a : β) : (s.sum fun (i : ι) => f i • a) = (s.sum fun (i : ι) => f i) • a

theorem Finset.prod_pow_eq_pow_sum {ι : Type u_1} {β : Type u_4} [CommMonoid β] (s : Finset ι) (f : ι → ℕ) (a : β) : (s.prod fun (i : ι) => a ^ f i) = a ^ s.sum fun (i : ι) => f i

theorem Finset.sum_powersetCard {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (n : ℕ) (s : Finset α) (f : ℕ → β) : ((Finset.powersetCard n s).sum fun (t : Finset α) => f t.card) = s.card.choose n • f n

A sum over Finset.powersetCard which only depends on the size of the sets is constant.

theorem Finset.prod_powersetCard {α : Type u_3} {β : Type u_4} [CommMonoid β] (n : ℕ) (s : Finset α) (f : ℕ → β) : ((Finset.powersetCard n s).prod fun (t : Finset α) => f t.card) = f n ^ s.card.choose n

A product over Finset.powersetCard which only depends on the size of the sets is constant.

theorem Finset.sum_flip {β : Type u_4} [AddCommMonoid β] {n : ℕ} (f : ℕ → β) : ((Finset.range (n + 1)).sum fun (r : ℕ) => f (n - r)) = (Finset.range (n + 1)).sum fun (k : ℕ) => f k

theorem Finset.prod_flip {β : Type u_4} [CommMonoid β] {n : ℕ} (f : ℕ → β) : ((Finset.range (n + 1)).prod fun (r : ℕ) => f (n - r)) = (Finset.range (n + 1)).prod fun (k : ℕ) => f k

theorem Finset.sum_involution {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {f : α → β} (g : (a : α) → a ∈ s → α) : (∀ (a : α) (ha : a ∈ s), f a + f (g a ha) = 0) → (∀ (a : α) (ha : a ∈ s), f a ≠ 0 → g a ha ≠ a) → ∀ (g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s), (∀ (a : α) (ha : a ∈ s), g (g a ha) ⋯ = a) → (s.sum fun (x : α) => f x) = 0

abbrev Finset.sum_involution.match_1 {α : Type u_1} (s : Finset α) (motive : s.Nonempty → Prop) : ∀ (x : s.Nonempty), (∀ (x : α) (hx : x ∈ s), motive ⋯) → motive x

Equations

• ⋯ = ⋯

theorem Finset.prod_involution {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {f : α → β} (g : (a : α) → a ∈ s → α) : (∀ (a : α) (ha : a ∈ s), f a * f (g a ha) = 1) → (∀ (a : α) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a) → ∀ (g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s), (∀ (a : α) (ha : a ∈ s), g (g a ha) ⋯ = a) → (s.prod fun (x : α) => f x) = 1

theorem Finset.sum_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [AddCommMonoid β] [DecidableEq γ] (f : γ → β) (g : α → γ) : (s.sum fun (a : α) => f (g a)) = (Finset.image g s).sum fun (b : γ) => (Finset.filter (fun (a : α) => g a = b) s).card • f b

The sum of the composition of functions f and g, is the sum over b ∈ s.image g of f b times of the cardinality of the fibre of b. See also Finset.sum_image.

theorem Finset.prod_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [CommMonoid β] [DecidableEq γ] (f : γ → β) (g : α → γ) : (s.prod fun (a : α) => f (g a)) = (Finset.image g s).prod fun (b : γ) => f b ^ (Finset.filter (fun (a : α) => g a = b) s).card

The product of the composition of functions f and g, is the product over b ∈ s.image g of f b to the power of the cardinality of the fibre of b. See also Finset.prod_image.

theorem Finset.sum_piecewise {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (t : Finset α) (f : α → β) (g : α → β) : (s.sum fun (x : α) => t.piecewise f g x) = ((s ∩ t).sum fun (x : α) => f x) + (s \ t).sum fun (x : α) => g x

theorem Finset.prod_piecewise {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (t : Finset α) (f : α → β) (g : α → β) : (s.prod fun (x : α) => t.piecewise f g x) = ((s ∩ t).prod fun (x : α) => f x) * (s \ t).prod fun (x : α) => g x

theorem Finset.sum_inter_add_sum_diff {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (t : Finset α) (f : α → β) : (((s ∩ t).sum fun (x : α) => f x) + (s \ t).sum fun (x : α) => f x) = s.sum fun (x : α) => f x

theorem Finset.prod_inter_mul_prod_diff {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (t : Finset α) (f : α → β) : (((s ∩ t).prod fun (x : α) => f x) * (s \ t).prod fun (x : α) => f x) = s.prod fun (x : α) => f x

theorem Finset.sum_eq_add_sum_diff_singleton {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) : (s.sum fun (x : α) => f x) = f i + (s \ {i}).sum fun (x : α) => f x

theorem Finset.prod_eq_mul_prod_diff_singleton {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) : (s.prod fun (x : α) => f x) = f i * (s \ {i}).prod fun (x : α) => f x

theorem Finset.sum_eq_sum_diff_singleton_add {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) : (s.sum fun (x : α) => f x) = ((s \ {i}).sum fun (x : α) => f x) + f i

theorem Finset.prod_eq_prod_diff_singleton_mul {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) : (s.prod fun (x : α) => f x) = ((s \ {i}).prod fun (x : α) => f x) * f i

theorem Fintype.sum_eq_add_sum_compl {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] [Fintype α] (a : α) (f : α → β) : (Finset.univ.sum fun (i : α) => f i) = f a + {a}ᶜ.sum fun (i : α) => f i

theorem Fintype.prod_eq_mul_prod_compl {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] [Fintype α] (a : α) (f : α → β) : (Finset.univ.prod fun (i : α) => f i) = f a * {a}ᶜ.prod fun (i : α) => f i

theorem Fintype.sum_eq_sum_compl_add {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] [Fintype α] (a : α) (f : α → β) : (Finset.univ.sum fun (i : α) => f i) = ({a}ᶜ.sum fun (i : α) => f i) + f a

theorem Fintype.prod_eq_prod_compl_mul {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] [Fintype α] (a : α) (f : α → β) : (Finset.univ.prod fun (i : α) => f i) = ({a}ᶜ.prod fun (i : α) => f i) * f a

theorem Finset.dvd_prod_of_mem {α : Type u_3} {β : Type u_4} [CommMonoid β] (f : α → β) {a : α} {s : Finset α} (ha : a ∈ s) : f a ∣ s.prod fun (i : α) => f i

theorem Finset.sum_partition {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] (R : Setoid α) [DecidableRel Setoid.r] : (s.sum fun (x : α) => f x) = (Finset.image Quotient.mk'' s).sum fun (xbar : Quotient R) => (Finset.filter (fun (x : α) => ⟦x⟧ = xbar) s).sum fun (y : α) => f y

A sum can be partitioned into a sum of sums, each equivalent under a setoid.

theorem Finset.prod_partition {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] (R : Setoid α) [DecidableRel Setoid.r] : (s.prod fun (x : α) => f x) = (Finset.image Quotient.mk'' s).prod fun (xbar : Quotient R) => (Finset.filter (fun (x : α) => ⟦x⟧ = xbar) s).prod fun (y : α) => f y

A product can be partitioned into a product of products, each equivalent under a setoid.

theorem Finset.sum_cancels_of_partition_cancels {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] (R : Setoid α) [DecidableRel Setoid.r] (h : ∀ x ∈ s, ((Finset.filter (fun (y : α) => y ≈ x) s).sum fun (a : α) => f a) = 0) : (s.sum fun (x : α) => f x) = 0

If we can partition a sum into subsets that cancel out, then the whole sum cancels.

theorem Finset.prod_cancels_of_partition_cancels {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] (R : Setoid α) [DecidableRel Setoid.r] (h : ∀ x ∈ s, ((Finset.filter (fun (y : α) => y ≈ x) s).prod fun (a : α) => f a) = 1) : (s.prod fun (x : α) => f x) = 1

If we can partition a product into subsets that cancel out, then the whole product cancels.

theorem Finset.sum_update_of_not_mem {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∉ s) (f : α → β) (b : β) : (s.sum fun (x : α) => Function.update f i b x) = s.sum fun (x : α) => f x

theorem Finset.prod_update_of_not_mem {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∉ s) (f : α → β) (b : β) : (s.prod fun (x : α) => Function.update f i b x) = s.prod fun (x : α) => f x

theorem Finset.sum_update_of_mem {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) (b : β) : (s.sum fun (x : α) => Function.update f i b x) = b + (s \ {i}).sum fun (x : α) => f x

theorem Finset.prod_update_of_mem {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) (b : β) : (s.prod fun (x : α) => Function.update f i b x) = b * (s \ {i}).prod fun (x : α) => f x

theorem Finset.eq_of_card_le_one_of_sum_eq {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} (hc : s.card ≤ 1) {f : α → β} {b : β} (h : (s.sum fun (x : α) => f x) = b) (x : α) : x ∈ s → f x = b

If a sum of a Finset of size at most 1 has a given value, so do the terms in that sum.

theorem Finset.eq_of_card_le_one_of_prod_eq {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} (hc : s.card ≤ 1) {f : α → β} {b : β} (h : (s.prod fun (x : α) => f x) = b) (x : α) : x ∈ s → f x = b

If a product of a Finset of size at most 1 has a given value, so do the terms in that product.

theorem Finset.add_sum_erase {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) {a : α} (h : a ∈ s) : (f a + (s.erase a).sum fun (x : α) => f x) = s.sum fun (x : α) => f x

Taking a sum over s : Finset α is the same as adding the value on a single element f a to the sum over s.erase a.

See Multiset.sum_map_erase for the Multiset version.

theorem Finset.mul_prod_erase {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) {a : α} (h : a ∈ s) : (f a * (s.erase a).prod fun (x : α) => f x) = s.prod fun (x : α) => f x

Taking a product over s : Finset α is the same as multiplying the value on a single element f a by the product of s.erase a.

See Multiset.prod_map_erase for the Multiset version.

theorem Finset.sum_erase_add {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) {a : α} (h : a ∈ s) : ((s.erase a).sum fun (x : α) => f x) + f a = s.sum fun (x : α) => f x

A variant of Finset.add_sum_erase with the addition swapped.

theorem Finset.prod_erase_mul {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) {a : α} (h : a ∈ s) : ((s.erase a).prod fun (x : α) => f x) * f a = s.prod fun (x : α) => f x

A variant of Finset.mul_prod_erase with the multiplication swapped.

theorem Finset.sum_erase {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) {f : α → β} {a : α} (h : f a = 0) : ((s.erase a).sum fun (x : α) => f x) = s.sum fun (x : α) => f x

If a function applied at a point is 0, a sum is unchanged by removing that point, if present, from a Finset.

theorem Finset.prod_erase {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) {f : α → β} {a : α} (h : f a = 1) : ((s.erase a).prod fun (x : α) => f x) = s.prod fun (x : α) => f x

If a function applied at a point is 1, a product is unchanged by removing that point, if present, from a Finset.

theorem Finset.sum_ite_zero {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (p : α → Prop) [DecidablePred p] (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : β) : (s.sum fun (i : α) => if p i then a else 0) = if ∃ i ∈ s, p i then a else 0

See also Finset.sum_boole.

theorem Finset.prod_ite_one {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (p : α → Prop) [DecidablePred p] (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : β) : (s.prod fun (i : α) => if p i then a else 1) = if ∃ i ∈ s, p i then a else 1

See also Finset.prod_boole.

theorem Finset.sum_erase_lt_of_pos {α : Type u_3} {γ : Type u_6} [DecidableEq α] [OrderedAddCommMonoid γ] [CovariantClass γ γ (fun (x x_1 : γ) => x + x_1) fun (x x_1 : γ) => x < x_1] {s : Finset α} {d : α} (hd : d ∈ s) {f : α → γ} (hdf : 0 < f d) : ((s.erase d).sum fun (m : α) => f m) < s.sum fun (m : α) => f m

theorem Finset.prod_erase_lt_of_one_lt {α : Type u_3} {γ : Type u_6} [DecidableEq α] [OrderedCommMonoid γ] [CovariantClass γ γ (fun (x x_1 : γ) => x * x_1) fun (x x_1 : γ) => x < x_1] {s : Finset α} {d : α} (hd : d ∈ s) {f : α → γ} (hdf : 1 < f d) : ((s.erase d).prod fun (m : α) => f m) < s.prod fun (m : α) => f m

theorem Finset.eq_zero_of_sum_eq_zero {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {f : α → β} {a : α} (hp : (s.sum fun (x : α) => f x) = 0) (h1 : ∀ x ∈ s, x ≠ a → f x = 0) (x : α) : x ∈ s → f x = 0

If a sum is 0 and the function is 0 except possibly at one point, it is 0 everywhere on the Finset.

theorem Finset.eq_one_of_prod_eq_one {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {f : α → β} {a : α} (hp : (s.prod fun (x : α) => f x) = 1) (h1 : ∀ x ∈ s, x ≠ a → f x = 1) (x : α) : x ∈ s → f x = 1

If a product is 1 and the function is 1 except possibly at one point, it is 1 everywhere on the Finset.

theorem Finset.sum_boole_nsmul {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) (a : α) : (s.sum fun (x : α) => (if a = x then 1 else 0) • f x) = if a ∈ s then f a else 0

theorem Finset.prod_pow_boole {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) (a : α) : (s.prod fun (x : α) => f x ^ if a = x then 1 else 0) = if a ∈ s then f a else 1

theorem Finset.prod_dvd_prod_of_dvd {α : Type u_3} {β : Type u_4} [CommMonoid β] {S : Finset α} (g1 : α → β) (g2 : α → β) (h : ∀ a ∈ S, g1 a ∣ g2 a) : S.prod g1 ∣ S.prod g2

theorem Finset.prod_dvd_prod_of_subset {ι : Type u_6} {M : Type u_7} [CommMonoid M] (s : Finset ι) (t : Finset ι) (f : ι → M) (h : s ⊆ t) : (s.prod fun (i : ι) => f i) ∣ t.prod fun (i : ι) => f i

theorem Finset.sum_sdiff_eq_sum_sdiff_iff {ι : Type u_1} {α : Type u_3} [DecidableEq ι] [AddCancelCommMonoid α] {s : Finset ι} {t : Finset ι} {f : ι → α} : (((s \ t).sum fun (i : ι) => f i) = (t \ s).sum fun (i : ι) => f i) ↔ (s.sum fun (i : ι) => f i) = t.sum fun (i : ι) => f i

theorem Finset.prod_sdiff_eq_prod_sdiff_iff {ι : Type u_1} {α : Type u_3} [DecidableEq ι] [CancelCommMonoid α] {s : Finset ι} {t : Finset ι} {f : ι → α} : (((s \ t).prod fun (i : ι) => f i) = (t \ s).prod fun (i : ι) => f i) ↔ (s.prod fun (i : ι) => f i) = t.prod fun (i : ι) => f i

theorem Finset.sum_sdiff_ne_sum_sdiff_iff {ι : Type u_1} {α : Type u_3} [DecidableEq ι] [AddCancelCommMonoid α] {s : Finset ι} {t : Finset ι} {f : ι → α} : (((s \ t).sum fun (i : ι) => f i) ≠ (t \ s).sum fun (i : ι) => f i) ↔ (s.sum fun (i : ι) => f i) ≠ t.sum fun (i : ι) => f i

theorem Finset.prod_sdiff_ne_prod_sdiff_iff {ι : Type u_1} {α : Type u_3} [DecidableEq ι] [CancelCommMonoid α] {s : Finset ι} {t : Finset ι} {f : ι → α} : (((s \ t).prod fun (i : ι) => f i) ≠ (t \ s).prod fun (i : ι) => f i) ↔ (s.prod fun (i : ι) => f i) ≠ t.prod fun (i : ι) => f i

theorem Finset.card_eq_sum_ones {α : Type u_3} (s : Finset α) : s.card = s.sum fun (x : α) => 1

theorem Finset.sum_const_nat {α : Type u_3} {s : Finset α} {m : ℕ} {f : α → ℕ} (h₁ : ∀ x ∈ s, f x = m) : (s.sum fun (x : α) => f x) = s.card * m

theorem Finset.sum_card_fiberwise_eq_card_filter {ι : Type u_1} {κ : Type u_6} [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) : (t.sum fun (j : κ) => (Finset.filter (fun (i : ι) => g i = j) s).card) = (Finset.filter (fun (i : ι) => g i ∈ t) s).card

theorem Finset.card_filter {α : Type u_3} (p : α → Prop) [DecidablePred p] (s : Finset α) : (Finset.filter p s).card = s.sum fun (a : α) => if p a then 1 else 0

@[simp]

theorem Finset.op_sum {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} (f : α → β) : MulOpposite.op (s.sum fun (x : α) => f x) = s.sum fun (x : α) => 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 : α → βᵐᵒᵖ) : (s.sum fun (x : α) => f x).unop = s.sum fun (x : α) => (f x).unop

@[simp]

theorem Finset.sum_neg_distrib {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [SubtractionCommMonoid β] : (s.sum fun (x : α) => -f x) = -s.sum fun (x : α) => f x

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem Finset.sum_sdiff_eq_sub {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [AddCommGroup β] [DecidableEq α] (h : s₁ ⊆ s₂) : ((s₂ \ s₁).sum fun (x : α) => f x) = (s₂.sum fun (x : α) => f x) - s₁.sum fun (x : α) => f x

@[simp]

theorem Finset.prod_sdiff_eq_div {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [CommGroup β] [DecidableEq α] (h : s₁ ⊆ s₂) : ((s₂ \ s₁).prod fun (x : α) => f x) = (s₂.prod fun (x : α) => f x) / s₁.prod fun (x : α) => f x

theorem Finset.sum_sdiff_sub_sum_sdiff {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [AddCommGroup β] [DecidableEq α] : (((s₂ \ s₁).sum fun (x : α) => f x) - (s₁ \ s₂).sum fun (x : α) => f x) = (s₂.sum fun (x : α) => f x) - s₁.sum fun (x : α) => f x

theorem Finset.prod_sdiff_div_prod_sdiff {α : Type u_3} {β : Type u_4} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [CommGroup β] [DecidableEq α] : (((s₂ \ s₁).prod fun (x : α) => f x) / (s₁ \ s₂).prod fun (x : α) => f x) = (s₂.prod fun (x : α) => f x) / s₁.prod fun (x : α) => f x

@[simp]

theorem Finset.sum_erase_eq_sub {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommGroup β] [DecidableEq α] {a : α} (h : a ∈ s) : ((s.erase a).sum fun (x : α) => f x) = (s.sum fun (x : α) => f x) - f a

@[simp]

theorem Finset.prod_erase_eq_div {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommGroup β] [DecidableEq α] {a : α} (h : a ∈ s) : ((s.erase a).prod fun (x : α) => f x) = (s.prod fun (x : α) => f x) / f a

@[simp]

theorem Finset.card_sigma {α : Type u_3} {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) : (s.sigma t).card = s.sum fun (a : α) => (t a).card

@[simp]

theorem Finset.card_disjiUnion {α : Type u_3} {β : Type u_4} (s : Finset α) (t : α → Finset β) (h : (↑s).PairwiseDisjoint t) : (s.disjiUnion t h).card = s.sum fun (i : α) => (t i).card

theorem Finset.card_biUnion {α : Type u_3} {β : Type u_4} [DecidableEq β] {s : Finset α} {t : α → Finset β} (h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → Disjoint (t x) (t y)) : (s.biUnion t).card = s.sum fun (u : α) => (t u).card

theorem Finset.card_biUnion_le {α : Type u_3} {β : Type u_4} [DecidableEq β] {s : Finset α} {t : α → Finset β} : (s.biUnion t).card ≤ s.sum fun (a : α) => (t a).card

theorem Finset.card_eq_sum_card_fiberwise {α : Type u_3} {β : Type u_4} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β} (H : ∀ x ∈ s, f x ∈ t) : s.card = t.sum fun (a : β) => (Finset.filter (fun (x : α) => f x = a) s).card

theorem Finset.card_eq_sum_card_image {α : Type u_3} {β : Type u_4} [DecidableEq β] (f : α → β) (s : Finset α) : s.card = (Finset.image f s).sum fun (a : β) => (Finset.filter (fun (x : α) => f x = a) s).card

theorem Finset.mem_sum {α : Type u_3} {β : Type u_4} {f : α → Multiset β} (s : Finset α) (b : β) : (b ∈ s.sum fun (x : α) => f x) ↔ ∃ a ∈ s, b ∈ f a

theorem Finset.prod_eq_zero {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [CommMonoidWithZero β] (ha : a ∈ s) (h : f a = 0) : (s.prod fun (x : α) => f x) = 0

theorem Finset.prod_boole {α : Type u_3} {β : Type u_4} [CommMonoidWithZero β] {s : Finset α} {p : α → Prop} [DecidablePred p] : (s.prod fun (i : α) => if p i then 1 else 0) = if ∀ i ∈ s, p i then 1 else 0

theorem Finset.support_prod_subset {ι : Type u_1} {α : Type u_3} {β : Type u_4} [CommMonoidWithZero β] (s : Finset ι) (f : ι → α → β) : (Function.support fun (x : α) => s.prod fun (i : ι) => f i x) ⊆ ⋂ i ∈ s, Function.support (f i)

theorem Finset.prod_eq_zero_iff {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoidWithZero β] [Nontrivial β] [NoZeroDivisors β] : (s.prod fun (x : α) => f x) = 0 ↔ ∃ a ∈ s, f a = 0

theorem Finset.prod_ne_zero_iff {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoidWithZero β] [Nontrivial β] [NoZeroDivisors β] : (s.prod fun (x : α) => f x) ≠ 0 ↔ ∀ a ∈ s, f a ≠ 0

theorem Finset.support_prod {ι : Type u_1} {α : Type u_3} {β : Type u_4} [CommMonoidWithZero β] [Nontrivial β] [NoZeroDivisors β] (s : Finset ι) (f : ι → α → β) : (Function.support fun (x : α) => s.prod fun (i : ι) => f i x) = ⋂ i ∈ s, Function.support (f i)

theorem Finset.sum_unique_nonempty {α : Type u_6} {β : Type u_7} [AddCommMonoid β] [Unique α] (s : Finset α) (f : α → β) (h : s.Nonempty) : (s.sum fun (x : α) => f x) = f default

theorem Finset.prod_unique_nonempty {α : Type u_6} {β : Type u_7} [CommMonoid β] [Unique α] (s : Finset α) (f : α → β) (h : s.Nonempty) : (s.prod fun (x : α) => f x) = f default

theorem Finset.sum_nat_mod {α : Type u_3} (s : Finset α) (n : ℕ) (f : α → ℕ) : (s.sum fun (i : α) => f i) % n = (s.sum fun (i : α) => f i % n) % n

theorem Finset.prod_nat_mod {α : Type u_3} (s : Finset α) (n : ℕ) (f : α → ℕ) : (s.prod fun (i : α) => f i) % n = (s.prod fun (i : α) => f i % n) % n

theorem Finset.sum_int_mod {α : Type u_3} (s : Finset α) (n : ℤ) (f : α → ℤ) : (s.sum fun (i : α) => f i) % n = (s.sum fun (i : α) => f i % n) % n

theorem Finset.prod_int_mod {α : Type u_3} (s : Finset α) (n : ℤ) (f : α → ℤ) : (s.prod fun (i : α) => f i) % n = (s.prod fun (i : α) => f i % n) % n

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)) : (Finset.univ.sum fun (x : ι) => f x) = Finset.univ.sum fun (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 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)) : (Finset.univ.prod fun (x : ι) => f x) = Finset.univ.prod fun (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 Function.Bijective.finset_prod {ι : 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)) : (Finset.univ.prod fun (x : ι) => f x) = Finset.univ.prod fun (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 : Function.Bijective e) (f : ι → α) (g : κ → α) (h : ∀ (x : ι), f x = g (e x)) : (Finset.univ.sum fun (x : ι) => f x) = Finset.univ.sum fun (x : κ) => g x

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)) : (Finset.univ.sum fun (x : ι) => f x) = Finset.univ.sum fun (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 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)) : (Finset.univ.prod fun (x : ι) => f x) = Finset.univ.prod fun (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 Function.Bijective.sum_comp {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] {e : ι → κ} (he : Function.Bijective e) (g : κ → α) : (Finset.univ.sum fun (i : ι) => g (e i)) = Finset.univ.sum fun (i : κ) => g i

theorem Function.Bijective.prod_comp {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommMonoid α] {e : ι → κ} (he : Function.Bijective e) (g : κ → α) : (Finset.univ.prod fun (i : ι) => g (e i)) = Finset.univ.prod fun (i : κ) => g i

theorem Equiv.sum_comp {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] (e : ι ≃ κ) (g : κ → α) : (Finset.univ.sum fun (i : ι) => g (e i)) = Finset.univ.sum fun (i : κ) => g i

theorem Equiv.prod_comp {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommMonoid α] (e : ι ≃ κ) (g : κ → α) : (Finset.univ.prod fun (i : ι) => g (e i)) = Finset.univ.prod fun (i : κ) => g i

theorem Fintype.sum_of_injective {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] (e : ι → κ) (he : Function.Injective e) (f : ι → α) (g : κ → α) (h' : ∀ i ∉ Set.range e, g i = 0) (h : ∀ (i : ι), f i = g (e i)) : (Finset.univ.sum fun (i : ι) => f i) = Finset.univ.sum fun (j : κ) => g j

theorem Fintype.prod_of_injective {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommMonoid α] (e : ι → κ) (he : Function.Injective e) (f : ι → α) (g : κ → α) (h' : ∀ i ∉ Set.range e, g i = 1) (h : ∀ (i : ι), f i = g (e i)) : (Finset.univ.prod fun (i : ι) => f i) = Finset.univ.prod fun (j : κ) => g j

theorem Fintype.sum_fiberwise {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] [DecidableEq κ] (g : ι → κ) (f : ι → α) : (Finset.univ.sum fun (j : κ) => Finset.univ.sum fun (i : { i : ι // g i = j }) => f ↑i) = Finset.univ.sum fun (i : ι) => f i

theorem Fintype.prod_fiberwise {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommMonoid α] [DecidableEq κ] (g : ι → κ) (f : ι → α) : (Finset.univ.prod fun (j : κ) => Finset.univ.prod fun (i : { i : ι // g i = j }) => f ↑i) = Finset.univ.prod fun (i : ι) => f i

theorem Fintype.sum_fiberwise' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] [DecidableEq κ] (g : ι → κ) (f : κ → α) : (Finset.univ.sum fun (j : κ) => Finset.univ.sum fun (_i : { i : ι // g i = j }) => f j) = Finset.univ.sum fun (i : ι) => f (g i)

theorem Fintype.prod_fiberwise' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommMonoid α] [DecidableEq κ] (g : ι → κ) (f : κ → α) : (Finset.univ.prod fun (j : κ) => Finset.univ.prod fun (_i : { i : ι // g i = j }) => f j) = Finset.univ.prod fun (i : ι) => f (g i)

theorem Fintype.sum_unique {α : Type u_9} {β : Type u_10} [AddCommMonoid β] [Unique α] [Fintype α] (f : α → β) : (Finset.univ.sum fun (x : α) => f x) = f default

theorem Fintype.prod_unique {α : Type u_9} {β : Type u_10} [CommMonoid β] [Unique α] [Fintype α] (f : α → β) : (Finset.univ.prod fun (x : α) => f x) = f default

theorem Fintype.sum_empty {α : Type u_9} {β : Type u_10} [AddCommMonoid β] [IsEmpty α] [Fintype α] (f : α → β) : (Finset.univ.sum fun (x : α) => f x) = 0

theorem Fintype.prod_empty {α : Type u_9} {β : Type u_10} [CommMonoid β] [IsEmpty α] [Fintype α] (f : α → β) : (Finset.univ.prod fun (x : α) => f x) = 1

theorem Fintype.sum_subsingleton {α : Type u_9} {β : Type u_10} [AddCommMonoid β] [Subsingleton α] [Fintype α] (f : α → β) (a : α) : (Finset.univ.sum fun (x : α) => f x) = f a

theorem Fintype.prod_subsingleton {α : Type u_9} {β : Type u_10} [CommMonoid β] [Subsingleton α] [Fintype α] (f : α → β) (a : α) : (Finset.univ.prod fun (x : α) => f x) = f a

theorem Fintype.sum_subtype_add_sum_subtype {α : Type u_9} {β : Type u_10} [Fintype α] [AddCommMonoid β] (p : α → Prop) (f : α → β) [DecidablePred p] : ((Finset.univ.sum fun (i : { x : α // p x }) => f ↑i) + Finset.univ.sum fun (i : { x : α // ¬p x }) => f ↑i) = Finset.univ.sum fun (i : α) => f i

theorem Fintype.prod_subtype_mul_prod_subtype {α : Type u_9} {β : Type u_10} [Fintype α] [CommMonoid β] (p : α → Prop) (f : α → β) [DecidablePred p] : ((Finset.univ.prod fun (i : { x : α // p x }) => f ↑i) * Finset.univ.prod fun (i : { x : α // ¬p x }) => f ↑i) = Finset.univ.prod fun (i : α) => f i

theorem Fintype.sum_subset {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] {s : Finset ι} {f : ι → α} (h : ∀ (i : ι), f i ≠ 0 → i ∈ s) : (s.sum fun (i : ι) => f i) = Finset.univ.sum fun (i : ι) => f i

theorem Fintype.prod_subset {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] {s : Finset ι} {f : ι → α} (h : ∀ (i : ι), f i ≠ 1 → i ∈ s) : (s.prod fun (i : ι) => f i) = Finset.univ.prod fun (i : ι) => f i

theorem Fintype.sum_ite_eq_ite_exists {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] (p : ι → Prop) [DecidablePred p] (h : ∀ (i j : ι), p i → p j → i = j) (a : α) : (Finset.univ.sum fun (i : ι) => if p i then a else 0) = if ∃ (i : ι), p i then a else 0

theorem Fintype.prod_ite_eq_ite_exists {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] (p : ι → Prop) [DecidablePred p] (h : ∀ (i j : ι), p i → p j → i = j) (a : α) : (Finset.univ.prod fun (i : ι) => if p i then a else 1) = if ∃ (i : ι), p i then a else 1

theorem Fintype.sum_dite_eq {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] [DecidableEq ι] (i : ι) (f : (j : ι) → i = j → α) : (Finset.univ.sum fun (j : ι) => if h : i = j then f j h else 0) = f i ⋯

See also Finset.sum_dite_eq.

theorem Fintype.prod_dite_eq {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] [DecidableEq ι] (i : ι) (f : (j : ι) → i = j → α) : (Finset.univ.prod fun (j : ι) => if h : i = j then f j h else 1) = f i ⋯

See also Finset.prod_dite_eq.

theorem Fintype.sum_dite_eq' {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] [DecidableEq ι] (i : ι) (f : (j : ι) → j = i → α) : (Finset.univ.sum fun (j : ι) => if h : j = i then f j h else 0) = f i ⋯

See also Finset.sum_dite_eq'.

theorem Fintype.prod_dite_eq' {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] [DecidableEq ι] (i : ι) (f : (j : ι) → j = i → α) : (Finset.univ.prod fun (j : ι) => if h : j = i then f j h else 1) = f i ⋯

See also Finset.prod_dite_eq'.

theorem Fintype.sum_ite_eq {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] [DecidableEq ι] (i : ι) (f : ι → α) : (Finset.univ.sum fun (j : ι) => if i = j then f j else 0) = f i

See also Finset.sum_ite_eq.

theorem Fintype.prod_ite_eq {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] [DecidableEq ι] (i : ι) (f : ι → α) : (Finset.univ.prod fun (j : ι) => if i = j then f j else 1) = f i

See also Finset.prod_ite_eq.

theorem Fintype.sum_ite_eq' {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] [DecidableEq ι] (i : ι) (f : ι → α) : (Finset.univ.sum fun (j : ι) => if j = i then f j else 0) = f i

See also Finset.sum_ite_eq'.

theorem Fintype.prod_ite_eq' {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] [DecidableEq ι] (i : ι) (f : ι → α) : (Finset.univ.prod fun (j : ι) => if j = i then f j else 1) = f i

See also Finset.prod_ite_eq'.

theorem Fintype.sum_pi_single {ι : Type u_6} [Fintype ι] [DecidableEq ι] {α : ι → Type u_9} [(i : ι) → AddCommMonoid (α i)] (i : ι) (f : (i : ι) → α i) : (Finset.univ.sum fun (j : ι) => Pi.single j (f j) i) = f i

See also Finset.sum_pi_single.

theorem Fintype.prod_pi_mulSingle {ι : Type u_6} [Fintype ι] [DecidableEq ι] {α : ι → Type u_9} [(i : ι) → CommMonoid (α i)] (i : ι) (f : (i : ι) → α i) : (Finset.univ.prod fun (j : ι) => Pi.mulSingle j (f j) i) = f i

See also Finset.prod_pi_mulSingle.

theorem Fintype.sum_pi_single' {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] [DecidableEq ι] (i : ι) (a : α) : (Finset.univ.sum fun (j : ι) => Pi.single i a j) = a

See also Finset.sum_pi_single'.

theorem Fintype.prod_pi_mulSingle' {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] [DecidableEq ι] (i : ι) (a : α) : (Finset.univ.prod fun (j : ι) => Pi.mulSingle i a j) = a

See also Finset.prod_pi_mulSingle'.

theorem Fintype.prod_boole {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoidWithZero α] {p : ι → Prop} [DecidablePred p] : (Finset.univ.prod fun (i : ι) => if p i then 1 else 0) = if ∀ (i : ι), p i then 1 else 0

@[simp]

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

@[simp]

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

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

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

theorem List.sum_toFinset {α : Type u_3} {M : Type u_6} [DecidableEq α] [AddCommMonoid M] (f : α → M) {l : List α} (_hl : l.Nodup) : l.toFinset.sum f = (List.map f l).sum

abbrev List.sum_toFinset.match_2 {α : Type u_1} (a : α) (l : List α) (motive : a ∉ l ∧ l.Nodup → Prop) : ∀ (x : a ∉ l ∧ l.Nodup), (∀ (not_mem : a ∉ l) (hl : l.Nodup), motive ⋯) → motive x

Equations

• ⋯ = ⋯

abbrev List.sum_toFinset.match_1 {α : Type u_1} (motive : (x : List α) → x.Nodup → Prop) : ∀ (x : List α) (x_1 : x.Nodup), (∀ (x : [].Nodup), motive [] x) → (∀ (a : α) (l : List α) (hl : (a :: l).Nodup), motive (a :: l) hl) → motive x x_1

Equations

• ⋯ = ⋯

theorem List.prod_toFinset {α : Type u_3} {M : Type u_6} [DecidableEq α] [CommMonoid M] (f : α → M) {l : List α} (_hl : l.Nodup) : l.toFinset.prod f = (List.map f l).prod

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

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

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

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

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

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

@[simp]

theorem Multiset.toFinset_sum_count_eq {α : Type u_3} [DecidableEq α] (s : Multiset α) : (s.toFinset.sum fun (a : α) => Multiset.count a s) = Multiset.card s

@[simp]

theorem Multiset.sum_count_eq {α : Type u_3} [DecidableEq α] [Fintype α] (s : Multiset α) : (Finset.univ.sum fun (a : α) => Multiset.count a s) = Multiset.card s

theorem Multiset.count_sum' {α : Type u_3} {β : Type u_4} [DecidableEq α] {s : Finset β} {a : α} {f : β → Multiset α} : Multiset.count a (s.sum fun (x : β) => f x) = s.sum fun (x : β) => Multiset.count a (f x)

@[simp]

theorem Multiset.toFinset_sum_count_nsmul_eq {α : Type u_3} [DecidableEq α] (s : Multiset α) : (s.toFinset.sum fun (a : α) => Multiset.count a s • {a}) = s

theorem Multiset.exists_smul_of_dvd_count {α : Type u_3} [DecidableEq α] (s : Multiset α) {k : ℕ} (h : ∀ a ∈ s, k ∣ Multiset.count a s) : ∃ (u : Multiset α), s = k • u

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

theorem Multiset.sum_sum {α : Type u_6} {ι : Type u_7} [AddCommMonoid α] (f : ι → Multiset α) (s : Finset ι) : (s.sum fun (x : ι) => f x).sum = s.sum fun (x : ι) => (f x).sum

theorem Multiset.prod_sum {α : Type u_6} {ι : Type u_7} [CommMonoid α] (f : ι → Multiset α) (s : Finset ι) : (s.sum fun (x : ι) => f x).prod = s.prod fun (x : ι) => (f x).prod

@[simp]

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

theorem Units.mk0_prod {α : Type u_3} {β : Type u_4} [CommGroupWithZero β] (s : Finset α) (f : α → β) (h : (s.prod fun (b : α) => f b) ≠ 0) : Units.mk0 (s.prod fun (b : α) => f b) h = s.attach.prod fun (b : { x : α // x ∈ s }) => Units.mk0 (f ↑b) ⋯

theorem nat_abs_sum_le {ι : Type u_6} (s : Finset ι) (f : ι → ℤ) : (s.sum fun (i : ι) => f i).natAbs ≤ s.sum fun (i : ι) => (f i).natAbs

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 (s.prod fun (i : ι) => f i) = s.sum fun (i : ι) => Additive.ofMul (f i)

@[simp]

theorem toMul_sum {ι : Type u_1} {α : Type u_3} [CommMonoid α] (s : Finset ι) (f : ι → Additive α) : Additive.toMul (s.sum fun (i : ι) => f i) = s.prod fun (i : ι) => 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 (s.sum fun (i : ι) => f i) = s.prod fun (i : ι) => Multiplicative.ofAdd (f i)

@[simp]

theorem toAdd_prod {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] (s : Finset ι) (f : ι → Multiplicative α) : Multiplicative.toAdd (s.prod fun (i : ι) => f i) = s.sum fun (i : ι) => Multiplicative.toAdd (f i)

@[deprecated Fintype.prod_equiv]

theorem Equiv.prod_comp' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommMonoid α] (e : ι ≃ κ) (f : ι → α) (g : κ → α) (h : ∀ (x : ι), f x = g (e x)) : (Finset.univ.prod fun (x : ι) => f x) = Finset.univ.prod fun (x : κ) => g x

Alias of Fintype.prod_equiv.

---

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.

@[deprecated Fintype.sum_equiv]

theorem Equiv.sum_comp' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] (e : ι ≃ κ) (f : ι → α) (g : κ → α) (h : ∀ (x : ι), f x = g (e x)) : (Finset.univ.sum fun (x : ι) => f x) = Finset.univ.sum fun (x : κ) => g x

Alias of Fintype.sum_equiv.

---

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.