# Documentation

Mathlib.Algebra.BigOperators.Basic

# 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 in s, f x is notation for Finset.prod s f (assuming β is a CommMonoid)
• ∑ x in 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} {α : Type v} [inst : ] (s : ) (f : αβ) :
β

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

Equations
def Finset.prod {β : Type u} {α : Type v} [inst : ] (s : ) (f : αβ) :
β

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

Equations
@[simp]
theorem Finset.sum_mk {β : Type u} {α : Type v} [inst : ] (s : ) (hs : ) (f : αβ) :
Finset.sum { val := s, nodup := hs } f = Multiset.sum ()
@[simp]
theorem Finset.prod_mk {β : Type u} {α : Type v} [inst : ] (s : ) (hs : ) (f : αβ) :
Finset.prod { val := s, nodup := hs } f =
@[simp]
theorem Finset.sum_val {α : Type v} [inst : ] (s : ) :
@[simp]
theorem Finset.prod_val {α : Type v} [inst : ] (s : ) :

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

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

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

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

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

∏ x, f x is notation for Finset.prod 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.
theorem Finset.sum_eq_multiset_sum {β : Type u} {α : Type v} [inst : ] (s : ) (f : αβ) :
(Finset.sum s fun x => f x) = Multiset.sum (Multiset.map f s.val)
theorem Finset.prod_eq_multiset_prod {β : Type u} {α : Type v} [inst : ] (s : ) (f : αβ) :
(Finset.prod s fun x => f x) = Multiset.prod (Multiset.map f s.val)
theorem Finset.sum_eq_fold {β : Type u} {α : Type v} [inst : ] (s : ) (f : αβ) :
(Finset.sum s fun x => f x) = Finset.fold (fun x x_1 => x + x_1) 0 f s
theorem Finset.prod_eq_fold {β : Type u} {α : Type v} [inst : ] (s : ) (f : αβ) :
(Finset.prod s fun x => f x) = Finset.fold (fun x x_1 => x * x_1) 1 f s
@[simp]
theorem Finset.sum_multiset_singleton {α : Type v} (s : ) :
(Finset.sum s fun x => {x}) = s.val
theorem map_sum {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] {G : Type u_1} [inst : ] (g : G) (f : αβ) (s : ) :
g (Finset.sum s fun x => f x) = Finset.sum s fun x => g (f x)
theorem map_prod {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] {G : Type u_1} [inst : ] (g : G) (f : αβ) (s : ) :
g (Finset.prod s fun x => f x) = Finset.prod s fun x => g (f x)
theorem AddMonoidHom.map_sum {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] (g : β →+ γ) (f : αβ) (s : ) :
g (Finset.sum s fun x => f x) = Finset.sum s fun x => g (f x)

Deprecated: use _root_.map_sum instead.

theorem MonoidHom.map_prod {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] (g : β →* γ) (f : αβ) (s : ) :
g (Finset.prod s fun x => f x) = Finset.prod s fun x => g (f x)

Deprecated: use _root_.map_prod instead.

theorem AddEquiv.map_sum {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] (g : β ≃+ γ) (f : αβ) (s : ) :
g (Finset.sum s fun x => f x) = Finset.sum s fun x => g (f x)

Deprecated: use _root_.map_sum instead.

theorem MulEquiv.map_prod {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] (g : β ≃* γ) (f : αβ) (s : ) :
g (Finset.prod s fun x => f x) = Finset.prod s fun x => g (f x)

Deprecated: use _root_.map_prod instead.

theorem RingHom.map_list_prod {β : Type u} {γ : Type w} [inst : ] [inst : ] (f : β →+* γ) (l : List β) :
f () = List.prod (List.map (f) l)
theorem RingHom.map_list_sum {β : Type u} {γ : Type w} [inst : ] [inst : ] (f : β →+* γ) (l : List β) :
f () = List.sum (List.map (f) l)
theorem RingHom.unop_map_list_prod {β : Type u} {γ : Type w} [inst : ] [inst : ] (f : β →+* γᵐᵒᵖ) (l : List β) :
(f ()).unop = List.prod (List.reverse (List.map (MulOpposite.unop f) l))

A morphism into the opposite ring acts on the product by acting on the reversed elements.

theorem RingHom.map_multiset_prod {β : Type u} {γ : Type w} [inst : ] [inst : ] (f : β →+* γ) (s : ) :
f () = Multiset.prod (Multiset.map (f) s)
theorem RingHom.map_multiset_sum {β : Type u} {γ : Type w} [inst : ] [inst : ] (f : β →+* γ) (s : ) :
f () = Multiset.sum (Multiset.map (f) s)
theorem RingHom.map_prod {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] (g : β →+* γ) (f : αβ) (s : ) :
g (Finset.prod s fun x => f x) = Finset.prod s fun x => g (f x)
theorem RingHom.map_sum {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] (g : β →+* γ) (f : αβ) (s : ) :
g (Finset.sum s fun x => f x) = Finset.sum s fun x => g (f x)
theorem AddMonoidHom.coe_finset_sum {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] (f : αβ →+ γ) (s : ) :
↑(Finset.sum s fun x => f x) = Finset.sum s fun x => ↑(f x)
theorem MonoidHom.coe_finset_prod {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] (f : αβ →* γ) (s : ) :
↑(Finset.prod s fun x => f x) = Finset.prod s fun x => ↑(f x)
@[simp]
theorem AddMonoidHom.finset_sum_apply {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] (f : αβ →+ γ) (s : ) (b : β) :
↑(Finset.sum s fun x => f x) b = Finset.sum s fun x => ↑(f x) b
@[simp]
theorem MonoidHom.finset_prod_apply {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] (f : αβ →* γ) (s : ) (b : β) :
↑(Finset.prod s fun x => f x) b = Finset.prod s fun x => ↑(f x) b
@[simp]
theorem Finset.sum_empty {β : Type u} {α : Type v} {f : αβ} [inst : ] :
(Finset.sum fun x => f x) = 0
@[simp]
theorem Finset.prod_empty {β : Type u} {α : Type v} {f : αβ} [inst : ] :
(Finset.prod fun x => f x) = 1
theorem Finset.sum_of_empty {β : Type u} {α : Type v} {f : αβ} [inst : ] [inst : ] (s : ) :
(Finset.sum s fun i => f i) = 0
theorem Finset.prod_of_empty {β : Type u} {α : Type v} {f : αβ} [inst : ] [inst : ] (s : ) :
(Finset.prod s fun i => f i) = 1
@[simp]
theorem Finset.sum_cons {β : Type u} {α : Type v} {s : } {a : α} {f : αβ} [inst : ] (h : ¬a s) :
(Finset.sum (Finset.cons a s h) fun x => f x) = f a + Finset.sum s fun x => f x
@[simp]
theorem Finset.prod_cons {β : Type u} {α : Type v} {s : } {a : α} {f : αβ} [inst : ] (h : ¬a s) :
(Finset.prod (Finset.cons a s h) fun x => f x) = f a * Finset.prod s fun x => f x
@[simp]
theorem Finset.sum_insert {β : Type u} {α : Type v} {s : } {a : α} {f : αβ} [inst : ] [inst : ] :
¬a s(Finset.sum (insert a s) fun x => f x) = f a + Finset.sum s fun x => f x
@[simp]
theorem Finset.prod_insert {β : Type u} {α : Type v} {s : } {a : α} {f : αβ} [inst : ] [inst : ] :
¬a s(Finset.prod (insert a s) fun x => f x) = f a * Finset.prod s fun x => f x
@[simp]
theorem Finset.sum_insert_of_eq_zero_if_not_mem {β : Type u} {α : Type v} {s : } {a : α} {f : αβ} [inst : ] [inst : ] (h : ¬a sf a = 0) :
(Finset.sum (insert a s) fun x => f x) = Finset.sum s 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} {α : Type v} {s : } {a : α} {f : αβ} [inst : ] [inst : ] (h : ¬a sf a = 1) :
(Finset.prod (insert a s) fun x => f x) = Finset.prod s 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} {α : Type v} {s : } {a : α} {f : αβ} [inst : ] [inst : ] (h : f a = 0) :
(Finset.sum (insert a s) fun x => f x) = Finset.sum s 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} {α : Type v} {s : } {a : α} {f : αβ} [inst : ] [inst : ] (h : f a = 1) :
(Finset.prod (insert a s) fun x => f x) = Finset.prod s 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.

@[simp]
theorem Finset.sum_singleton {β : Type u} {α : Type v} {a : α} {f : αβ} [inst : ] :
(Finset.sum {a} fun x => f x) = f a
@[simp]
theorem Finset.prod_singleton {β : Type u} {α : Type v} {a : α} {f : αβ} [inst : ] :
(Finset.prod {a} fun x => f x) = f a
theorem Finset.sum_pair {β : Type u} {α : Type v} {f : αβ} [inst : ] [inst : ] {a : α} {b : α} (h : a b) :
(Finset.sum {a, b} fun x => f x) = f a + f b
theorem Finset.prod_pair {β : Type u} {α : Type v} {f : αβ} [inst : ] [inst : ] {a : α} {b : α} (h : a b) :
(Finset.prod {a, b} fun x => f x) = f a * f b
@[simp]
theorem Finset.sum_const_zero {β : Type u} {α : Type v} {s : } [inst : ] :
(Finset.sum s fun _x => 0) = 0
@[simp]
theorem Finset.prod_const_one {β : Type u} {α : Type v} {s : } [inst : ] :
(Finset.prod s fun _x => 1) = 1
@[simp]
theorem Finset.sum_image {β : Type u} {α : Type v} {γ : Type w} {f : αβ} [inst : ] [inst : ] {s : } {g : γα} :
(∀ (x : γ), x s∀ (y : γ), y sg x = g yx = y) → (Finset.sum () fun x => f x) = Finset.sum s fun x => f (g x)
@[simp]
theorem Finset.prod_image {β : Type u} {α : Type v} {γ : Type w} {f : αβ} [inst : ] [inst : ] {s : } {g : γα} :
(∀ (x : γ), x s∀ (y : γ), y sg x = g yx = y) → (Finset.prod () fun x => f x) = Finset.prod s fun x => f (g x)
@[simp]
theorem Finset.sum_map {β : Type u} {α : Type v} {γ : Type w} [inst : ] (s : ) (e : α γ) (f : γβ) :
(Finset.sum () fun x => f x) = Finset.sum s fun x => f (e x)
@[simp]
theorem Finset.prod_map {β : Type u} {α : Type v} {γ : Type w} [inst : ] (s : ) (e : α γ) (f : γβ) :
(Finset.prod () fun x => f x) = Finset.prod s fun x => f (e x)
theorem Finset.sum_congr {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} {g : αβ} [inst : ] (h : s₁ = s₂) :
(∀ (x : α), x s₂f x = g x) → Finset.sum s₁ f = Finset.sum s₂ g
theorem Finset.prod_congr {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} {g : αβ} [inst : ] (h : s₁ = s₂) :
(∀ (x : α), x s₂f x = g x) → Finset.prod s₁ f = Finset.prod s₂ g
theorem Finset.sum_disjUnion {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [inst : ] (h : Disjoint s₁ s₂) :
(Finset.sum (Finset.disjUnion s₁ s₂ h) fun x => f x) = (Finset.sum s₁ fun x => f x) + Finset.sum s₂ fun x => f x
theorem Finset.prod_disjUnion {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [inst : ] (h : Disjoint s₁ s₂) :
(Finset.prod (Finset.disjUnion s₁ s₂ h) fun x => f x) = (Finset.prod s₁ fun x => f x) * Finset.prod s₂ fun x => f x
theorem Finset.sum_disjUnionᵢ {ι : Type u_1} {β : Type u} {α : Type v} {f : αβ} [inst : ] (s : ) (t : ι) (h : Set.PairwiseDisjoint (s) t) :
(Finset.sum () fun x => f x) = Finset.sum s fun i => Finset.sum (t i) fun x => f x
theorem Finset.prod_disjUnionᵢ {ι : Type u_1} {β : Type u} {α : Type v} {f : αβ} [inst : ] (s : ) (t : ι) (h : Set.PairwiseDisjoint (s) t) :
(Finset.prod () fun x => f x) = Finset.prod s fun i => Finset.prod (t i) fun x => f x
theorem Finset.sum_union_inter {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [inst : ] [inst : ] :
((Finset.sum (s₁ s₂) fun x => f x) + Finset.sum (s₁ s₂) fun x => f x) = (Finset.sum s₁ fun x => f x) + Finset.sum s₂ fun x => f x
theorem Finset.prod_union_inter {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [inst : ] [inst : ] :
((Finset.prod (s₁ s₂) fun x => f x) * Finset.prod (s₁ s₂) fun x => f x) = (Finset.prod s₁ fun x => f x) * Finset.prod s₂ fun x => f x
theorem Finset.sum_union {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [inst : ] [inst : ] (h : Disjoint s₁ s₂) :
(Finset.sum (s₁ s₂) fun x => f x) = (Finset.sum s₁ fun x => f x) + Finset.sum s₂ fun x => f x
theorem Finset.prod_union {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [inst : ] [inst : ] (h : Disjoint s₁ s₂) :
(Finset.prod (s₁ s₂) fun x => f x) = (Finset.prod s₁ fun x => f x) * Finset.prod s₂ fun x => f x
theorem Finset.sum_filter_add_sum_filter_not {β : Type u} {α : Type v} [inst : ] (s : ) (p : αProp) [inst : ] [inst : (x : α) → Decidable ¬p x] (f : αβ) :
((Finset.sum () fun x => f x) + Finset.sum (Finset.filter (fun x => ¬p x) s) fun x => f x) = Finset.sum s fun x => f x
theorem Finset.prod_filter_mul_prod_filter_not {β : Type u} {α : Type v} [inst : ] (s : ) (p : αProp) [inst : ] [inst : (x : α) → Decidable ¬p x] (f : αβ) :
((Finset.prod () fun x => f x) * Finset.prod (Finset.filter (fun x => ¬p x) s) fun x => f x) = Finset.prod s fun x => f x
@[simp]
theorem Finset.sum_to_list {β : Type u} {α : Type v} [inst : ] (s : ) (f : αβ) :
@[simp]
theorem Finset.prod_to_list {β : Type u} {α : Type v} [inst : ] (s : ) (f : αβ) :
theorem Equiv.Perm.sum_comp {β : Type u} {α : Type v} [inst : ] (σ : ) (s : ) (f : αβ) (hs : { a | σ a a } s) :
(Finset.sum s fun x => f (σ x)) = Finset.sum s fun x => f x
theorem Equiv.Perm.prod_comp {β : Type u} {α : Type v} [inst : ] (σ : ) (s : ) (f : αβ) (hs : { a | σ a a } s) :
(Finset.prod s fun x => f (σ x)) = Finset.prod s fun x => f x
theorem Equiv.Perm.sum_comp' {β : Type u} {α : Type v} [inst : ] (σ : ) (s : ) (f : ααβ) (hs : { a | σ a a } s) :
(Finset.sum s fun x => f (σ x) x) = Finset.sum s fun x => f x (↑() x)
theorem Equiv.Perm.prod_comp' {β : Type u} {α : Type v} [inst : ] (σ : ) (s : ) (f : ααβ) (hs : { a | σ a a } s) :
(Finset.prod s fun x => f (σ x) x) = Finset.prod s fun x => f x (↑() x)
theorem IsCompl.sum_add_sum {β : Type u} {α : Type v} [inst : ] [inst : ] {s : } {t : } (h : IsCompl s t) (f : αβ) :
((Finset.sum s fun i => f i) + Finset.sum t fun i => f i) = Finset.sum Finset.univ fun i => f i
theorem IsCompl.prod_mul_prod {β : Type u} {α : Type v} [inst : ] [inst : ] {s : } {t : } (h : IsCompl s t) (f : αβ) :
((Finset.prod s fun i => f i) * Finset.prod t fun i => f i) = Finset.prod Finset.univ fun i => f i
theorem Finset.sum_add_sum_compl {β : Type u} {α : Type v} [inst : ] [inst : ] [inst : ] (s : ) (f : αβ) :
((Finset.sum s fun i => f i) + Finset.sum (s) fun i => f i) = Finset.sum Finset.univ 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} {α : Type v} [inst : ] [inst : ] [inst : ] (s : ) (f : αβ) :
((Finset.prod s fun i => f i) * Finset.prod (s) fun i => f i) = Finset.prod Finset.univ 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} {α : Type v} [inst : ] [inst : ] [inst : ] (s : ) (f : αβ) :
((Finset.sum (s) fun i => f i) + Finset.sum s fun i => f i) = Finset.sum Finset.univ fun i => f i
theorem Finset.prod_compl_mul_prod {β : Type u} {α : Type v} [inst : ] [inst : ] [inst : ] (s : ) (f : αβ) :
((Finset.prod (s) fun i => f i) * Finset.prod s fun i => f i) = Finset.prod Finset.univ fun i => f i
theorem Finset.sum_sdiff {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [inst : ] [inst : ] (h : s₁ s₂) :
((Finset.sum (s₂ \ s₁) fun x => f x) + Finset.sum s₁ fun x => f x) = Finset.sum s₂ fun x => f x
theorem Finset.prod_sdiff {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [inst : ] [inst : ] (h : s₁ s₂) :
((Finset.prod (s₂ \ s₁) fun x => f x) * Finset.prod s₁ fun x => f x) = Finset.prod s₂ fun x => f x
@[simp]
theorem Finset.sum_disj_sum {β : Type u} {α : Type v} {γ : Type w} [inst : ] (s : ) (t : ) (f : α γβ) :
(Finset.sum () fun x => f x) = (Finset.sum s fun x => f ()) + Finset.sum t fun x => f ()
@[simp]
theorem Finset.prod_disj_sum {β : Type u} {α : Type v} {γ : Type w} [inst : ] (s : ) (t : ) (f : α γβ) :
(Finset.prod () fun x => f x) = (Finset.prod s fun x => f ()) * Finset.prod t fun x => f ()
theorem Finset.sum_sum_elim {β : Type u} {α : Type v} {γ : Type w} [inst : ] (s : ) (t : ) (f : αβ) (g : γβ) :
(Finset.sum () fun x => Sum.elim f g x) = (Finset.sum s fun x => f x) + Finset.sum t fun x => g x
theorem Finset.prod_sum_elim {β : Type u} {α : Type v} {γ : Type w} [inst : ] (s : ) (t : ) (f : αβ) (g : γβ) :
(Finset.prod () fun x => Sum.elim f g x) = (Finset.prod s fun x => f x) * Finset.prod t fun x => g x
theorem Finset.sum_bunionᵢ {β : Type u} {α : Type v} {γ : Type w} {f : αβ} [inst : ] [inst : ] {s : } {t : γ} (hs : Set.PairwiseDisjoint (s) t) :
(Finset.sum () fun x => f x) = Finset.sum s fun x => Finset.sum (t x) fun i => f i
theorem Finset.prod_bunionᵢ {β : Type u} {α : Type v} {γ : Type w} {f : αβ} [inst : ] [inst : ] {s : } {t : γ} (hs : Set.PairwiseDisjoint (s) t) :
(Finset.prod () fun x => f x) = Finset.prod s fun x => Finset.prod (t x) fun i => f i
theorem Finset.sum_sigma {β : Type u} {α : Type v} [inst : ] {σ : αType u_1} (s : ) (t : (a : α) → Finset (σ a)) (f : β) :
(Finset.sum () fun x => f x) = Finset.sum s fun a => Finset.sum (t a) fun s => f { fst := a, snd := 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} {α : Type v} [inst : ] {σ : αType u_1} (s : ) (t : (a : α) → Finset (σ a)) (f : β) :
(Finset.prod () fun x => f x) = Finset.prod s fun a => Finset.prod (t a) fun s => f { fst := a, snd := 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} {α : Type v} [inst : ] {σ : αType u_1} (s : ) (t : (a : α) → Finset (σ a)) (f : (a : α) → σ aβ) :
(Finset.sum s fun a => Finset.sum (t a) fun s => f a s) = Finset.sum () fun x => f x.fst x.snd
theorem Finset.prod_sigma' {β : Type u} {α : Type v} [inst : ] {σ : αType u_1} (s : ) (t : (a : α) → Finset (σ a)) (f : (a : α) → σ aβ) :
(Finset.prod s fun a => Finset.prod (t a) fun s => f a s) = Finset.prod () fun x => f x.fst x.snd
theorem Finset.sum_bij {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : αβ} {g : γβ} (i : (a : α) → a sγ) (hi : ∀ (a : α) (ha : a s), i a ha t) (h : ∀ (a : α) (ha : a s), f a = g (i a ha)) (i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ s) (ha₂ : a₂ s), i a₁ ha₁ = i a₂ ha₂a₁ = a₂) (i_surj : ∀ (b : γ), b ta ha, b = i a ha) :
(Finset.sum s fun x => f x) = Finset.sum t fun x => g x

Reorder a sum.

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

theorem Finset.prod_bij {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : αβ} {g : γβ} (i : (a : α) → a sγ) (hi : ∀ (a : α) (ha : a s), i a ha t) (h : ∀ (a : α) (ha : a s), f a = g (i a ha)) (i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ s) (ha₂ : a₂ s), i a₁ ha₁ = i a₂ ha₂a₁ = a₂) (i_surj : ∀ (b : γ), b ta ha, b = i a ha) :
(Finset.prod s fun x => f x) = Finset.prod t fun x => g x

Reorder a product.

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

theorem Finset.sum_bij' {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : αβ} {g : γβ} (i : (a : α) → a sγ) (hi : ∀ (a : α) (ha : a s), i a ha t) (h : ∀ (a : α) (ha : a s), f a = g (i a ha)) (j : (a : γ) → a tα) (hj : ∀ (a : γ) (ha : a t), j a ha s) (left_inv : ∀ (a : α) (ha : a s), j (i a ha) (hi a ha) = a) (right_inv : ∀ (a : γ) (ha : a t), i (j a ha) (hj a ha) = a) :
(Finset.sum s fun x => f x) = Finset.sum t fun x => g x

Reorder a sum.

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

theorem Finset.prod_bij' {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : αβ} {g : γβ} (i : (a : α) → a sγ) (hi : ∀ (a : α) (ha : a s), i a ha t) (h : ∀ (a : α) (ha : a s), f a = g (i a ha)) (j : (a : γ) → a tα) (hj : ∀ (a : γ) (ha : a t), j a ha s) (left_inv : ∀ (a : α) (ha : a s), j (i a ha) (hi a ha) = a) (right_inv : ∀ (a : γ) (ha : a t), i (j a ha) (hj a ha) = a) :
(Finset.prod s fun x => f x) = Finset.prod t fun x => g x

Reorder a product.

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

theorem Finset.Equiv.sum_comp_finset {ι : Type u_2} {β : Type u} [inst : ] {ι' : Type u_1} [inst : ] (e : ι ι') (f : ι'β) {s' : Finset ι'} {s : } (h : s = Finset.image (↑()) s') :
(Finset.sum s' fun i' => f i') = Finset.sum s fun i => f (e i)

Reindexing a sum over a finset along an equivalence. See Equiv.sum_comp for the version where s and s' are univ.

theorem Finset.Equiv.prod_comp_finset {ι : Type u_2} {β : Type u} [inst : ] {ι' : Type u_1} [inst : ] (e : ι ι') (f : ι'β) {s' : Finset ι'} {s : } (h : s = Finset.image (↑()) s') :
(Finset.prod s' fun i' => f i') = Finset.prod s fun i => f (e i)

Reindexing a product over a finset along an equivalence. See Equiv.prod_comp for the version where s and s' are univ.

theorem Finset.sum_finset_product {β : Type u} {α : Type v} {γ : Type w} [inst : ] (r : Finset (γ × α)) (s : ) (t : γ) (h : ∀ (p : γ × α), p r p.fst s p.snd t p.fst) {f : γ × αβ} :
(Finset.sum r fun p => f p) = Finset.sum s fun c => Finset.sum (t c) fun a => f (c, a)
theorem Finset.prod_finset_product {β : Type u} {α : Type v} {γ : Type w} [inst : ] (r : Finset (γ × α)) (s : ) (t : γ) (h : ∀ (p : γ × α), p r p.fst s p.snd t p.fst) {f : γ × αβ} :
(Finset.prod r fun p => f p) = Finset.prod s fun c => Finset.prod (t c) fun a => f (c, a)
theorem Finset.sum_finset_product' {β : Type u} {α : Type v} {γ : Type w} [inst : ] (r : Finset (γ × α)) (s : ) (t : γ) (h : ∀ (p : γ × α), p r p.fst s p.snd t p.fst) {f : γαβ} :
(Finset.sum r fun p => f p.fst p.snd) = Finset.sum s fun c => Finset.sum (t c) fun a => f c a
theorem Finset.prod_finset_product' {β : Type u} {α : Type v} {γ : Type w} [inst : ] (r : Finset (γ × α)) (s : ) (t : γ) (h : ∀ (p : γ × α), p r p.fst s p.snd t p.fst) {f : γαβ} :
(Finset.prod r fun p => f p.fst p.snd) = Finset.prod s fun c => Finset.prod (t c) fun a => f c a
theorem Finset.sum_finset_product_right {β : Type u} {α : Type v} {γ : Type w} [inst : ] (r : Finset (α × γ)) (s : ) (t : γ) (h : ∀ (p : α × γ), p r p.snd s p.fst t p.snd) {f : α × γβ} :
(Finset.sum r fun p => f p) = Finset.sum s fun c => Finset.sum (t c) fun a => f (a, c)
theorem Finset.prod_finset_product_right {β : Type u} {α : Type v} {γ : Type w} [inst : ] (r : Finset (α × γ)) (s : ) (t : γ) (h : ∀ (p : α × γ), p r p.snd s p.fst t p.snd) {f : α × γβ} :
(Finset.prod r fun p => f p) = Finset.prod s fun c => Finset.prod (t c) fun a => f (a, c)
theorem Finset.sum_finset_product_right' {β : Type u} {α : Type v} {γ : Type w} [inst : ] (r : Finset (α × γ)) (s : ) (t : γ) (h : ∀ (p : α × γ), p r p.snd s p.fst t p.snd) {f : αγβ} :
(Finset.sum r fun p => f p.fst p.snd) = Finset.sum s fun c => Finset.sum (t c) fun a => f a c
theorem Finset.prod_finset_product_right' {β : Type u} {α : Type v} {γ : Type w} [inst : ] (r : Finset (α × γ)) (s : ) (t : γ) (h : ∀ (p : α × γ), p r p.snd s p.fst t p.snd) {f : αγβ} :
(Finset.prod r fun p => f p.fst p.snd) = Finset.prod s fun c => Finset.prod (t c) fun a => f a c
theorem Finset.sum_fiberwise_of_maps_to {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] {s : } {t : } {g : αγ} (h : ∀ (x : α), x sg x t) (f : αβ) :
(Finset.sum t fun y => Finset.sum (Finset.filter (fun x => g x = y) s) fun x => f x) = Finset.sum s fun x => f x
theorem Finset.prod_fiberwise_of_maps_to {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] {s : } {t : } {g : αγ} (h : ∀ (x : α), x sg x t) (f : αβ) :
(Finset.prod t fun y => Finset.prod (Finset.filter (fun x => g x = y) s) fun x => f x) = Finset.prod s fun x => f x
abbrev Finset.sum_image'.match_1 {α : Type u_2} {γ : Type u_1} {s : } {g : γα} (_x : α) (motive : (a, a s g a = _x) → Prop) :
(x : a, a s g a = _x) → ((c : γ) → (hcs : c s) → (hc : g c = _x) → motive (_ : a, a s g a = _x)) → motive x
Equations
theorem Finset.sum_image' {β : Type u} {α : Type v} {γ : Type w} {f : αβ} [inst : ] [inst : ] {s : } {g : γα} (h : γβ) (eq : ∀ (c : γ), c sf (g c) = Finset.sum (Finset.filter (fun c' => g c' = g c) s) fun x => h x) :
(Finset.sum () fun x => f x) = Finset.sum s fun x => h x
theorem Finset.prod_image' {β : Type u} {α : Type v} {γ : Type w} {f : αβ} [inst : ] [inst : ] {s : } {g : γα} (h : γβ) (eq : ∀ (c : γ), c sf (g c) = Finset.prod (Finset.filter (fun c' => g c' = g c) s) fun x => h x) :
(Finset.prod () fun x => f x) = Finset.prod s fun x => h x
theorem Finset.sum_add_distrib {β : Type u} {α : Type v} {s : } {f : αβ} {g : αβ} [inst : ] :
(Finset.sum s fun x => f x + g x) = (Finset.sum s fun x => f x) + Finset.sum s fun x => g x
theorem Finset.prod_mul_distrib {β : Type u} {α : Type v} {s : } {f : αβ} {g : αβ} [inst : ] :
(Finset.prod s fun x => f x * g x) = (Finset.prod s fun x => f x) * Finset.prod s fun x => g x
theorem Finset.sum_product {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : γ × αβ} :
(Finset.sum (s ×ᶠ t) fun x => f x) = Finset.sum s fun x => Finset.sum t fun y => f (x, y)
theorem Finset.prod_product {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : γ × αβ} :
(Finset.prod (s ×ᶠ t) fun x => f x) = Finset.prod s fun x => Finset.prod t fun y => f (x, y)
theorem Finset.sum_product' {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : γαβ} :
(Finset.sum (s ×ᶠ t) fun x => f x.fst x.snd) = Finset.sum s fun x => Finset.sum t fun y => f x y

An uncurried version of Finset.sum_product

theorem Finset.prod_product' {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : γαβ} :
(Finset.prod (s ×ᶠ t) fun x => f x.fst x.snd) = Finset.prod s fun x => Finset.prod t fun y => f x y

An uncurried version of Finset.prod_product.

theorem Finset.sum_product_right {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : γ × αβ} :
(Finset.sum (s ×ᶠ t) fun x => f x) = Finset.sum t fun y => Finset.sum s fun x => f (x, y)
theorem Finset.prod_product_right {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : γ × αβ} :
(Finset.prod (s ×ᶠ t) fun x => f x) = Finset.prod t fun y => Finset.prod s fun x => f (x, y)
theorem Finset.sum_product_right' {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : γαβ} :
(Finset.sum (s ×ᶠ t) fun x => f x.fst x.snd) = Finset.sum t fun y => Finset.sum s fun x => f x y

An uncurried version of Finset.prod_product_right

theorem Finset.prod_product_right' {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : γαβ} :
(Finset.prod (s ×ᶠ t) fun x => f x.fst x.snd) = Finset.prod t fun y => Finset.prod s fun x => f x y

An uncurried version of Finset.prod_product_right.

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.sum_comm' {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : γ} {t' : } {s' : α} (h : ∀ (x : γ) (y : α), x s y t x x s' y y t') {f : γαβ} :
(Finset.sum s fun x => Finset.sum (t x) fun y => f x y) = Finset.sum t' fun y => Finset.sum (s' y) fun x => f x y

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

theorem Finset.prod_comm' {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : γ} {t' : } {s' : α} (h : ∀ (x : γ) (y : α), x s y t x x s' y y t') {f : γαβ} :
(Finset.prod s fun x => Finset.prod (t x) fun y => f x y) = Finset.prod t' fun y => Finset.prod (s' y) 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} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : γαβ} :
(Finset.sum s fun x => Finset.sum t fun y => f x y) = Finset.sum t fun y => Finset.sum s fun x => f x y
theorem Finset.prod_comm {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : γαβ} :
(Finset.prod s fun x => Finset.prod t fun y => f x y) = Finset.prod t fun y => Finset.prod s fun x => f x y
theorem Finset.sum_hom_rel {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] {r : βγProp} {f : αβ} {g : αγ} {s : } (h₁ : r 0 0) (h₂ : (a : α) → (b : β) → (c : γ) → r b cr (f a + b) (g a + c)) :
r (Finset.sum s fun x => f x) (Finset.sum s fun x => g x)
theorem Finset.prod_hom_rel {β : Type u} {α : Type v} {γ : Type w} [inst : ] [inst : ] {r : βγProp} {f : αβ} {g : αγ} {s : } (h₁ : r 1 1) (h₂ : (a : α) → (b : β) → (c : γ) → r b cr (f a * b) (g a * c)) :
r (Finset.prod s fun x => f x) (Finset.prod s fun x => g x)
theorem Finset.sum_eq_zero {β : Type u} {α : Type v} [inst : ] {f : αβ} {s : } (h : ∀ (x : α), x sf x = 0) :
(Finset.sum s fun x => f x) = 0
theorem Finset.prod_eq_one {β : Type u} {α : Type v} [inst : ] {f : αβ} {s : } (h : ∀ (x : α), x sf x = 1) :
(Finset.prod s fun x => f x) = 1
theorem Finset.sum_subset_zero_on_sdiff {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} {g : αβ} [inst : ] [inst : ] (h : s₁ s₂) (hg : ∀ (x : α), x s₂ \ s₁g x = 0) (hfg : ∀ (x : α), x s₁f x = g x) :
(Finset.sum s₁ fun i => f i) = Finset.sum s₂ fun i => g i
theorem Finset.prod_subset_one_on_sdiff {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} {g : αβ} [inst : ] [inst : ] (h : s₁ s₂) (hg : ∀ (x : α), x s₂ \ s₁g x = 1) (hfg : ∀ (x : α), x s₁f x = g x) :
(Finset.prod s₁ fun i => f i) = Finset.prod s₂ fun i => g i
theorem Finset.sum_subset {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [inst : ] (h : s₁ s₂) (hf : ∀ (x : α), x s₂¬x s₁f x = 0) :
(Finset.sum s₁ fun x => f x) = Finset.sum s₂ fun x => f x
theorem Finset.prod_subset {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [inst : ] (h : s₁ s₂) (hf : ∀ (x : α), x s₂¬x s₁f x = 1) :
(Finset.prod s₁ fun x => f x) = Finset.prod s₂ fun x => f x
theorem Finset.sum_filter_of_ne {β : Type u} {α : Type v} {s : } {f : αβ} [inst : ] {p : αProp} [inst : ] (hp : (x : α) → x sf x 0p x) :
(Finset.sum () fun x => f x) = Finset.sum s fun x => f x
theorem Finset.prod_filter_of_ne {β : Type u} {α : Type v} {s : } {f : αβ} [inst : ] {p : αProp} [inst : ] (hp : (x : α) → x sf x 1p x) :
(Finset.prod () fun x => f x) = Finset.prod s fun x => f x
theorem Finset.sum_filter_ne_zero {β : Type u} {α : Type v} {s : } {f : αβ} [inst : ] [inst : (x : α) → Decidable (f x 0)] :
(Finset.sum (Finset.filter (fun x => f x 0) s) fun x => f x) = Finset.sum s fun x => f x
theorem Finset.prod_filter_ne_one {β : Type u} {α : Type v} {s : } {f : αβ} [inst : ] [inst : (x : α) → Decidable (f x 1)] :
(Finset.prod (Finset.filter (fun x => f x 1) s) fun x => f x) = Finset.prod s fun x => f x
theorem Finset.sum_filter {β : Type u} {α : Type v} {s : } [inst : ] (p : αProp) [inst : ] (f : αβ) :
(Finset.sum () fun a => f a) = Finset.sum s fun a => if p a then f a else 0
theorem Finset.prod_filter {β : Type u} {α : Type v} {s : } [inst : ] (p : αProp) [inst : ] (f : αβ) :
(Finset.prod () fun a => f a) = Finset.prod s fun a => if p a then f a else 1
theorem Finset.sum_eq_single_of_mem {β : Type u} {α : Type v} [inst : ] {s : } {f : αβ} (a : α) (h : a s) (h₀ : ∀ (b : α), b sb af b = 0) :
(Finset.sum s fun x => f x) = f a
theorem Finset.prod_eq_single_of_mem {β : Type u} {α : Type v} [inst : ] {s : } {f : αβ} (a : α) (h : a s) (h₀ : ∀ (b : α), b sb af b = 1) :
(Finset.prod s fun x => f x) = f a
theorem Finset.sum_eq_single {β : Type u} {α : Type v} [inst : ] {s : } {f : αβ} (a : α) (h₀ : ∀ (b : α), b sb af b = 0) (h₁ : ¬a sf a = 0) :
(Finset.sum s fun x => f x) = f a
abbrev Finset.sum_eq_single.match_1 {α : Type u_1} {s : } (a : α) (motive : ¬a sProp) :
(x : ¬a s) → ((this : ¬a s) → motive this) → motive x
Equations
theorem Finset.prod_eq_single {β : Type u} {α : Type v} [inst : ] {s : } {f : αβ} (a : α) (h₀ : ∀ (b : α), b sb af b = 1) (h₁ : ¬a sf a = 1) :
(Finset.prod s fun x => f x) = f a
theorem Finset.sum_eq_add_of_mem {β : Type u} {α : Type v} [inst : ] {s : } {f : αβ} (a : α) (b : α) (ha : a s) (hb : b s) (hn : a b) (h₀ : ∀ (c : α), c sc a c bf c = 0) :
(Finset.sum s fun x => f x) = f a + f b
theorem Finset.prod_eq_mul_of_mem {β : Type u} {α : Type v} [inst : ] {s : } {f : αβ} (a : α) (b : α) (ha : a s) (hb : b s) (hn : a b) (h₀ : ∀ (c : α), c sc a c bf c = 1) :
(Finset.prod s fun x => f x) = f a * f b
theorem Finset.sum_eq_add {β : Type u} {α : Type v} [inst : ] {s : } {f : αβ} (a : α) (b : α) (hn : a b) (h₀ : ∀ (c : α), c sc a c bf c = 0) (ha : ¬a sf a = 0) (hb : ¬b sf b = 0) :
(Finset.sum s fun x => f x) = f a + f b
theorem Finset.prod_eq_mul {β : Type u} {α : Type v} [inst : ] {s : } {f : αβ} (a : α) (b : α) (hn : a b) (h₀ : ∀ (c : α), c sc a c bf c = 1) (ha : ¬a sf a = 1) (hb : ¬b sf b = 1) :
(Finset.prod s fun x => f x) = f a * f b
theorem Finset.sum_attach {β : Type u} {α : Type v} {s : } [inst : ] {f : αβ} :
(Finset.sum () fun x => f x) = Finset.sum s fun x => f x
theorem Finset.prod_attach {β : Type u} {α : Type v} {s : } [inst : ] {f : αβ} :
(Finset.prod () fun x => f x) = Finset.prod s fun x => f x
@[simp]
theorem Finset.sum_subtype_eq_sum_filter {β : Type u} {α : Type v} {s : } [inst : ] (f : αβ) {p : αProp} [inst : ] :
(Finset.sum () fun x => f x) = Finset.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} {α : Type v} {s : } [inst : ] (f : αβ) {p : αProp} [inst : ] :
(Finset.prod () fun x => f x) = Finset.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} {α : Type v} {s : } [inst : ] (f : αβ) {p : αProp} [inst : ] (h : (x : α) → x sp x) :
(Finset.sum () fun x => f x) = Finset.sum s 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} {α : Type v} {s : } [inst : ] (f : αβ) {p : αProp} [inst : ] (h : (x : α) → x sp x) :
(Finset.prod () fun x => f x) = Finset.prod s 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} {α : Type v} [inst : ] {p : αProp} {s : Finset { x // p x }} {f : { x // p x }β} {g : αβ} (h : ∀ (x : { x // p x }), x sg x = f x) :
(Finset.sum (Finset.map (Function.Embedding.subtype fun x => p x) s) fun x => g x) = Finset.sum s fun 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} {α : Type v} [inst : ] {p : αProp} {s : Finset { x // p x }} {f : { x // p x }β} {g : αβ} (h : ∀ (x : { x // p x }), x sg x = f x) :
(Finset.prod (Finset.map (Function.Embedding.subtype fun x => p x) s) fun x => g x) = Finset.prod s fun 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} {α : Type v} (s : ) [inst : ] (f : { x // x s }β) :
(Finset.sum Finset.univ fun i => f i) = Finset.sum () fun i => f i
theorem Finset.prod_coe_sort_eq_attach {β : Type u} {α : Type v} (s : ) [inst : ] (f : { x // x s }β) :
(Finset.prod Finset.univ fun i => f i) = Finset.prod () fun i => f i
theorem Finset.sum_coe_sort {β : Type u} {α : Type v} (s : ) (f : αβ) [inst : ] :
(Finset.sum Finset.univ fun i => f i) = Finset.sum s fun i => f i
theorem Finset.prod_coe_sort {β : Type u} {α : Type v} (s : ) (f : αβ) [inst : ] :
(Finset.prod Finset.univ fun i => f i) = Finset.prod s fun i => f i
theorem Finset.sum_finset_coe {β : Type u} {α : Type v} [inst : ] (f : αβ) (s : ) :
(Finset.sum Finset.univ fun i => f i) = Finset.sum s fun i => f i
theorem Finset.prod_finset_coe {β : Type u} {α : Type v} [inst : ] (f : αβ) (s : ) :
(Finset.prod Finset.univ fun i => f i) = Finset.prod s fun i => f i
theorem Finset.sum_subtype {β : Type u} {α : Type v} [inst : ] {p : αProp} {F : Fintype ()} (s : ) (h : ∀ (x : α), x s p x) (f : αβ) :
(Finset.sum s fun a => f a) = Finset.sum Finset.univ fun a => f a
theorem Finset.prod_subtype {β : Type u} {α : Type v} [inst : ] {p : αProp} {F : Fintype ()} (s : ) (h : ∀ (x : α), x s p x) (f : αβ) :
(Finset.prod s fun a => f a) = Finset.prod Finset.univ fun a => f a
theorem Finset.sum_congr_set {α : Type u_1} [inst : ] {β : Type u_2} [inst : ] (s : Set β) [inst : DecidablePred fun x => x s] (f : βα) (g : sα) (w : ∀ (x : β) (h : x s), f x = g { val := x, property := h }) (w' : ∀ (x : β), ¬x sf x = 0) :
Finset.sum Finset.univ f = Finset.sum Finset.univ 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} [inst : ] (s : Set β) [inst : DecidablePred fun x => x s] (motive : (x : { x // x s }) → x Finset.univProp) :
(x : { x // x s }) → (x_1 : x Finset.univ) → ((x : β) → (h : x s) → (x_2 : { val := x, property := h } Finset.univ) → motive { val := x, property := h } x_2) → motive x x_1
Equations
theorem Finset.prod_congr_set {α : Type u_1} [inst : ] {β : Type u_2} [inst : ] (s : Set β) [inst : DecidablePred fun x => x s] (f : βα) (g : sα) (w : ∀ (x : β) (h : x s), f x = g { val := x, property := h }) (w' : ∀ (x : β), ¬x sf x = 1) :
Finset.prod Finset.univ f = Finset.prod Finset.univ 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} {α : Type v} {γ : Type w} [inst : ] {s : } {p : αProp} {hp : } [inst : DecidablePred fun x => ¬p x] (f : (x : α) → p xγ) (g : (x : α) → ¬p xγ) (h : γβ) :
(Finset.sum s fun x => h (if hx : p x then f x hx else g x hx)) = (Finset.sum () fun x => h (f x (_ : x s p x).right)) + Finset.sum (Finset.attach (Finset.filter (fun x => ¬p x) s)) fun x => h (g x (_ : ¬p x))
theorem Finset.prod_apply_dite {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {p : αProp} {hp : } [inst : DecidablePred fun x => ¬p x] (f : (x : α) → p xγ) (g : (x : α) → ¬p xγ) (h : γβ) :
(Finset.prod s fun x => h (if hx : p x then f x hx else g x hx)) = (Finset.prod () fun x => h (f x (_ : x s p x).right)) * Finset.prod (Finset.attach (Finset.filter (fun x => ¬p x) s)) fun x => h (g x (_ : ¬p x))
theorem Finset.sum_apply_ite {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {p : αProp} {_hp : } (f : αγ) (g : αγ) (h : γβ) :
(Finset.sum s fun x => h (if p x then f x else g x)) = (Finset.sum () fun x => h (f x)) + Finset.sum (Finset.filter (fun x => ¬p x) s) fun x => h (g x)
theorem Finset.prod_apply_ite {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {p : αProp} {_hp : } (f : αγ) (g : αγ) (h : γβ) :
(Finset.prod s fun x => h (if p x then f x else g x)) = (Finset.prod () fun x => h (f x)) * Finset.prod (Finset.filter (fun x => ¬p x) s) fun x => h (g x)
theorem Finset.sum_dite {β : Type u} {α : Type v} [inst : ] {s : } {p : αProp} {hp : } (f : (x : α) → p xβ) (g : (x : α) → ¬p xβ) :
(Finset.sum s fun x => if hx : p x then f x hx else g x hx) = (Finset.sum () fun x => f x (_ : x s p x).right) + Finset.sum (Finset.attach (Finset.filter (fun x => ¬p x) s)) fun x => g x (_ : ¬p x)
theorem Finset.prod_dite {β : Type u} {α : Type v} [inst : ] {s : } {p : αProp} {hp : } (f : (x : α) → p xβ) (g : (x : α) → ¬p xβ) :
(Finset.prod s fun x => if hx : p x then f x hx else g x hx) = (Finset.prod () fun x => f x (_ : x s p x).right) * Finset.prod (Finset.attach (Finset.filter (fun x => ¬p x) s)) fun x => g x (_ : ¬p x)
theorem Finset.sum_ite {β : Type u} {α : Type v} [inst : ] {s : } {p : αProp} {hp : } (f : αβ) (g : αβ) :
(Finset.sum s fun x => if p x then f x else g x) = (Finset.sum () fun x => f x) + Finset.sum (Finset.filter (fun x => ¬p x) s) fun x => g x
theorem Finset.prod_ite {β : Type u} {α : Type v} [inst : ] {s : } {p : αProp} {hp : } (f : αβ) (g : αβ) :
(Finset.prod s fun x => if p x then f x else g x) = (Finset.prod () fun x => f x) * Finset.prod (Finset.filter (fun x => ¬p x) s) fun x => g x
theorem Finset.sum_ite_of_false {β : Type u} {α : Type v} {s : } [inst : ] {p : αProp} {hp : } (f : αβ) (g : αβ) (h : ∀ (x : α), x s¬p x) :
(Finset.sum s fun x => if p x then f x else g x) = Finset.sum s fun x => g x
theorem Finset.prod_ite_of_false {β : Type u} {α : Type v} {s : } [inst : ] {p : αProp} {hp : } (f : αβ) (g : αβ) (h : ∀ (x : α), x s¬p x) :
(Finset.prod s fun x => if p x then f x else g x) = Finset.prod s fun x => g x
theorem Finset.sum_ite_of_true {β : Type u} {α : Type v} {s : } [inst : ] {p : αProp} {hp : } (f : αβ) (g : αβ) (h : (x : α) → x sp x) :
(Finset.sum s fun x => if p x then f x else g x) = Finset.sum s fun x => f x
theorem Finset.prod_ite_of_true {β : Type u} {α : Type v} {s : } [inst : ] {p : αProp} {hp : } (f : αβ) (g : αβ) (h : (x : α) → x sp x) :
(Finset.prod s fun x => if p x then f x else g x) = Finset.prod s fun x => f x
theorem Finset.sum_apply_ite_of_false {β : Type u} {α : Type v} {γ : Type w} {s : } [inst : ] {p : αProp} {hp : } (f : αγ) (g : αγ) (k : γβ) (h : ∀ (x : α), x s¬p x) :
(Finset.sum s fun x => k (if p x then f x else g x)) = Finset.sum s fun x => k (g x)
theorem Finset.prod_apply_ite_of_false {β : Type u} {α : Type v} {γ : Type w} {s : } [inst : ] {p : αProp} {hp : } (f : αγ) (g : αγ) (k : γβ) (h : ∀ (x : α), x s¬p x) :
(Finset.prod s fun x => k (if p x then f x else g x)) = Finset.prod s fun x => k (g x)
theorem Finset.sum_apply_ite_of_true {β : Type u} {α : Type v} {γ : Type w} {s : } [inst : ] {p : αProp} {hp : } (f : αγ) (g : αγ) (k : γβ) (h : (x : α) → x sp x) :
(Finset.sum s fun x => k (if p x then f x else g x)) = Finset.sum s fun x => k (f x)
theorem Finset.prod_apply_ite_of_true {β : Type u} {α : Type v} {γ : Type w} {s : } [inst : ] {p : αProp} {hp : } (f : αγ) (g : αγ) (k : γβ) (h : (x : α) → x sp x) :
(Finset.prod s fun x => k (if p x then f x else g x)) = Finset.prod s fun x => k (f x)
theorem Finset.sum_extend_by_zero {β : Type u} {α : Type v} [inst : ] [inst : ] (s : ) (f : αβ) :
(Finset.sum s fun i => if i s then f i else 0) = Finset.sum s fun i => f i
theorem Finset.prod_extend_by_one {β : Type u} {α : Type v} [inst : ] [inst : ] (s : ) (f : αβ) :
(Finset.prod s fun i => if i s then f i else 1) = Finset.prod s fun i => f i
@[simp]
theorem Finset.sum_ite_mem {β : Type u} {α : Type v} [inst : ] [inst : ] (s : ) (t : ) (f : αβ) :
(Finset.sum s fun i => if i t then f i else 0) = Finset.sum (s t) fun i => f i
@[simp]
theorem Finset.prod_ite_mem {β : Type u} {α : Type v} [inst : ] [inst : ] (s : ) (t : ) (f : αβ) :
(Finset.prod s fun i => if i t then f i else 1) = Finset.prod (s t) fun i => f i
@[simp]
theorem Finset.sum_dite_eq {β : Type u} {α : Type v} [inst : ] [inst : ] (s : ) (a : α) (b : (x : α) → a = xβ) :
(Finset.sum s fun x => if h : a = x then b x h else 0) = if a s then b a (_ : a = a) else 0
@[simp]
theorem Finset.prod_dite_eq {β : Type u} {α : Type v} [inst : ] [inst : ] (s : ) (a : α) (b : (x : α) → a = xβ) :
(Finset.prod s fun x => if h : a = x then b x h else 1) = if a s then b a (_ : a = a) else 1
@[simp]
theorem Finset.sum_dite_eq' {β : Type u} {α : Type v} [inst : ] [inst : ] (s : ) (a : α) (b : (x : α) → x = aβ) :
(Finset.sum s fun x => if h : x = a then b x h else 0) = if a s then b a (_ : a = a) else 0
@[simp]
theorem Finset.prod_dite_eq' {β : Type u} {α : Type v} [inst : ] [inst : ] (s : ) (a : α) (b : (x : α) → x = aβ) :
(Finset.prod s fun x => if h : x = a then b x h else 1) = if a s then b a (_ : a = a) else 1
@[simp]
theorem Finset.sum_ite_eq {β : Type u} {α : Type v} [inst : ] [inst : ] (s : ) (a : α) (b : αβ) :
(Finset.sum s 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} {α : Type v} [inst : ] [inst : ] (s : ) (a : α) (b : αβ) :
(Finset.prod s 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} {α : Type v} [inst : ] [inst : ] (s : ) (a : α) (b : αβ) :
(Finset.sum s 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} {α : Type v} [inst : ] [inst : ] (s : ) (a : α) (b : αβ) :
(Finset.prod s 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} {α : Type v} [inst : ] (p : Prop) [inst : ] (s : ) (t : ) (f : αβ) :
(Finset.sum (if p then s else t) fun x => f x) = if p then Finset.sum s fun x => f x else Finset.sum t fun x => f x
theorem Finset.prod_ite_index {β : Type u} {α : Type v} [inst : ] (p : Prop) [inst : ] (s : ) (t : ) (f : αβ) :
(Finset.prod (if p then s else t) fun x => f x) = if p then Finset.prod s fun x => f x else Finset.prod t fun x => f x
@[simp]
theorem Finset.sum_ite_irrel {β : Type u} {α : Type v} [inst : ] (p : Prop) [inst : ] (s : ) (f : αβ) (g : αβ) :
(Finset.sum s fun x => if p then f x else g x) = if p then Finset.sum s fun x => f x else Finset.sum s fun x => g x
@[simp]
theorem Finset.prod_ite_irrel {β : Type u} {α : Type v} [inst : ] (p : Prop) [inst : ] (s : ) (f : αβ) (g : αβ) :
(Finset.prod s fun x => if p then f x else g x) = if p then Finset.prod s fun x => f x else Finset.prod s fun x => g x
@[simp]
theorem Finset.sum_dite_irrel {β : Type u} {α : Type v} [inst : ] (p : Prop) [inst : ] (s : ) (f : pαβ) (g : ¬pαβ) :
(Finset.sum s fun x => if h : p then f h x else g h x) = if h : p then Finset.sum s fun x => f h x else Finset.sum s fun x => g h x
@[simp]
theorem Finset.prod_dite_irrel {β : Type u} {α : Type v} [inst : ] (p : Prop) [inst : ] (s : ) (f : pαβ) (g : ¬pαβ) :
(Finset.prod s fun x => if h : p then f h x else g h x) = if h : p then Finset.prod s fun x => f h x else Finset.prod s fun x => g h x
@[simp]
theorem Finset.sum_pi_single' {ι : Type u_1} {M : Type u_2} [inst : ] [inst : ] (i : ι) (x : M) (s : ) :
(Finset.sum s fun j => Pi.single i x j) = if i s then x else 0
@[simp]
theorem Finset.sum_pi_single {ι : Type u_1} {M : ιType u_2} [inst : ] [inst : (i : ι) → AddCommMonoid (M i)] (i : ι) (f : (i : ι) → M i) (s : ) :
(Finset.sum s fun j => Pi.single j (f j) i) = if i s then f i else 0
theorem Finset.sum_bij_ne_zero {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : αβ} {g : γβ} (i : (a : α) → a sf a 0γ) (hi : ∀ (a : α) (h₁ : a s) (h₂ : f a 0), i a h₁ h₂ t) (i_inj : ∀ (a₁ a₂ : α) (h₁₁ : a₁ s) (h₁₂ : f a₁ 0) (h₂₁ : a₂ s) (h₂₂ : f a₂ 0), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂a₁ = a₂) (i_surj : ∀ (b : γ), b tg b 0a h₁ h₂, b = i a h₁ h₂) (h : ∀ (a : α) (h₁ : a s) (h₂ : f a 0), f a = g (i a h₁ h₂)) :
(Finset.sum s fun x => f x) = Finset.sum t fun x => g x
theorem Finset.prod_bij_ne_one {β : Type u} {α : Type v} {γ : Type w} [inst : ] {s : } {t : } {f : αβ} {g : γβ} (i : (a : α) → a sf a 1γ) (hi : ∀ (a : α) (h₁ : a s) (h₂ : f a 1), i a h₁ h₂ t) (i_inj : ∀ (a₁ a₂ : α) (h₁₁ : a₁ s) (h₁₂ : f a₁ 1) (h₂₁ : a₂ s) (h₂₂ : f a₂ 1), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂a₁ = a₂) (i_surj : ∀ (b : γ), b tg b 1a h₁ h₂, b = i a h₁ h₂) (h : ∀ (a : α) (h₁ : a s) (h₂ : f a 1), f a = g (i a h₁ h₂)) :
(Finset.prod s fun x => f x) = Finset.prod t fun x => g x
theorem Finset.sum_dite_of_false {β : Type u} {α : Type v} {s : } [inst : ] {p : αProp} {hp : } (h : ∀ (x : α), x s¬p x) (f : (x : α) → p xβ) (g : (x : α) → ¬p xβ) :
(Finset.sum s fun x => if hx : p x then f x hx else g x hx) = Finset.sum Finset.univ fun x => g (x) (h x (_ : x s))
theorem Finset.prod_dite_of_false {β : Type u} {α : Type v} {s : } [inst : ] {p : αProp} {hp : } (h : ∀ (x : α), x s¬p x) (f : (x : α) → p xβ) (g : (x : α) → ¬p xβ) :
(Finset.prod s fun x => if hx : p x then f x hx else g x hx) = Finset.prod Finset.univ fun x => g (x) (h x (_ : x s))
theorem Finset.sum_dite_of_true {β : Type u} {α : Type v} {s : } [inst : ] {p : αProp} {hp : } (h : (x : α) → x sp x) (f : (x : α) → p xβ) (g : (x : α) → ¬p xβ) :
(Finset.sum s fun x => if hx : p x then f x hx else g x hx) = Finset.sum Finset.univ fun x => f (x) (h x (_ : x s))
theorem Finset.prod_dite_of_true {β : Type u} {α : Type v} {s : } [inst : ] {p : αProp} {hp : } (h : (x : α) → x sp x) (f : (x : α) → p xβ) (g : (x : α) → ¬p xβ) :
(Finset.prod s fun x => if hx : p x then f x hx else g x hx) = Finset.prod Finset.univ fun x => f (x) (h x (_ : x s))
theorem Finset.nonempty_of_sum_ne_zero {β : Type u} {α : Type v} {s : } {f : αβ} [inst : ] (h : (Finset.sum s fun x => f x) 0) :
theorem Finset.nonempty_of_prod_ne_one {β : Type u} {α : Type v} {s : } {f : αβ} [inst : ] (h : (Finset.prod s fun x => f x) 1) :
theorem Finset.exists_ne_zero_of_sum_ne_zero {β : Type u} {α : Type v} {s : } {f : αβ} [inst : ] (h : (Finset.sum s fun x => f x) 0) :
a, a s f a 0
theorem Finset.exists_ne_one_of_prod_ne_one {β : Type u} {α : Type v} {s : } {f : αβ} [inst : ] (h : (Finset.prod s fun x => f x) 1) :
a, a s f a 1
theorem Finset.sum_range_succ_comm {β : Type u} [inst : ] (f : β) (n : ) :
(Finset.sum (Finset.range (n + 1)) fun x => f x) = f n + Finset.sum () fun x => f x
theorem Finset.prod_range_succ_comm {β : Type u} [inst : ] (f : β) (n : ) :
(Finset.prod (Finset.range (n + 1)) fun x => f x) = f n * Finset.prod () fun x => f x
theorem Finset.sum_range_succ {β : Type u} [inst : ] (f : β) (n : ) :
(Finset.sum (Finset.range (n + 1)) fun x => f x) = (Finset.sum () fun x => f x) + f n
theorem Finset.prod_range_succ {β : Type u} [inst : ] (f : β) (n : ) :
(Finset.prod (Finset.range (n + 1)) fun x => f x) = (Finset.prod () fun x => f x) * f n
abbrev Finset.sum_range_succ'.match_1 (motive : ) :
(x : ) → (Unitmotive 0) → ((n : ) → motive ()) → motive x
Equations
theorem Finset.sum_range_succ' {β : Type u} [inst : ] (f : β) (n : ) :
(Finset.sum (Finset.range (n + 1)) fun k => f k) = (Finset.sum () fun k => f (k + 1)) + f 0
theorem Finset.prod_range_succ' {β : Type u} [inst : ] (f : β) (n : ) :
(Finset.prod (Finset.range (n + 1)) fun k => f k) = (Finset.prod () fun k => f (k + 1)) * f 0
theorem Finset.eventually_constant_sum {β : Type u} [inst : ] {u : β} {N : } (hu : ∀ (n : ), n Nu n = 0) {n : } (hn : N n) :
(Finset.sum (Finset.range (n + 1)) fun k => u k) = Finset.sum (Finset.range (N + 1)) fun k => u k
theorem Finset.eventually_constant_prod {β : Type u} [inst : ] {u : β} {N : } (hu : ∀ (n : ), n Nu n = 1) {n : } (hn : N n) :
(Finset.prod (Finset.range (n + 1)) fun k => u k) = Finset.prod (Finset.range (N + 1)) fun k => u k
theorem Finset.sum_range_add {β : Type u} [inst : ] (f : β) (n : ) (m : ) :
(Finset.sum (Finset.range (n + m)) fun x => f x) = (Finset.sum () fun x => f x) + Finset.sum () fun x => f (n + x)
theorem Finset.prod_range_add {β : Type u} [inst : ] (f : β) (n : ) (m : ) :
(Finset.prod (Finset.range (n + m)) fun x => f x) = (Finset.prod () fun x => f x) * Finset.prod () fun x => f (n + x)
theorem Finset.sum_range_add_sub_sum_range {α : Type u_1} [inst : ] (f : α) (n : ) (m : ) :
((Finset.sum (Finset.range (n + m)) fun k => f k) - Finset.sum () fun k => f k) = Finset.sum () fun k => f (n + k)
theorem Finset.prod_range_add_div_prod_range {α : Type u_1} [inst : ] (f : α) (n : ) (m : ) :
((Finset.prod (Finset.range (n + m)) fun k => f k) / Finset.prod () fun k => f k) = Finset.prod () fun k => f (n + k)
theorem Finset.sum_range_zero {β : Type u} [inst : ] (f : β) :
(Finset.sum () fun k => f k) = 0
theorem Finset.prod_range_zero {β : Type u} [inst : ] (f : β) :
(Finset.prod () fun k => f k) = 1
theorem Finset.sum_range_one {β : Type u} [inst : ] (f : β) :
(Finset.sum () fun k => f k) = f 0
theorem Finset.prod_range_one {β : Type u} [inst : ] (f : β) :
(Finset.prod () fun k => f k) = f 0
theorem Finset.sum_list_map_count {α : Type v} [inst : ] (l : List α) {M : Type u_1} [inst : ] (f : αM) :
List.sum (List.map f l) = Finset.sum () fun m => f m
theorem Finset.prod_list_map_count {α : Type v} [inst : ] (l : List α) {M : Type u_1} [inst : ] (f : αM) :
List.prod (List.map f l) = Finset.prod () fun m => f m ^
theorem Finset.sum_list_count {α : Type v} [inst : ] [inst : ] (s : List α) :
= Finset.sum () fun m => m
theorem Finset.prod_list_count {α : Type v} [inst : ] [inst : ] (s : List α) :
= Finset.prod () fun m => m ^
theorem Finset.sum_list_count_of_subset {α : Type v} [inst : ] [inst : ] (m : List α) (s : ) (hs : ) :
= Finset.sum s fun i => i
theorem Finset.prod_list_count_of_subset {α : Type v} [inst : ] [inst : ] (m : List α) (s : ) (hs : ) :
= Finset.prod s fun i => i ^
theorem Finset.sum_filter_count_eq_countp {α : Type v} [inst : ] (p : αProp) [inst : ] (l : List α) :
(Finset.sum () fun x => ) = List.countp (fun b => decide (p b)) l
theorem Finset.sum_multiset_map_count {α : Type v} [inst : ] (s : ) {M : Type u_1} [inst : ] (f : αM) :
Multiset.sum () = Finset.sum () fun m => f m
theorem Finset.prod_multiset_map_count {α : Type v} [inst : ] (s : ) {M : Type u_1} [inst : ] (f : αM) :
= Finset.prod () fun m => f m ^
theorem Finset.sum_multiset_count {α : Type v} [inst : ] [inst : ] (s : ) :
= Finset.sum () fun m => m
theorem Finset.prod_multiset_count {α : Type v} [inst : ] [inst : ] (s : ) :
= Finset.prod () fun m => m ^
theorem Finset.sum_multiset_count_of_subset {α : Type v} [inst : ] [inst : ] (m : ) (s : ) (hs : ) :
= Finset.sum s fun i => i
theorem Finset.prod_multiset_count_of_subset {α : Type v} [inst : ] [inst : ] (m : ) (s : ) (hs : ) :
= Finset.prod s fun i => i ^
theorem Finset.sum_mem_multiset {β : Type u} {α : Type v} [inst : ] [inst : ] (m : ) (f : { x // x m }β) (g : αβ) (hfg : ∀ (x : { x // x m }), f x = g x) :
(Finset.sum Finset.univ fun x => f x) = Finset.sum () fun x => g x
theorem Finset.prod_mem_multiset {β : Type u} {α : Type v} [inst : ] [inst : ] (m : ) (f : { x // x m }β) (g : αβ) (hfg : ∀ (x : { x // x m }), f x = g x) :
(Finset.prod Finset.univ fun x => f x) = Finset.prod () fun x => g x
theorem Finset.sum_induction {α : Type v} {s : } {M : Type u_1} [inst : ] (f : αM) (p : MProp) (hom : (a b : M) → p ap bp (a + b)) (unit : p 0) (base : (x : α) → x sp (f x)) :
p (Finset.sum s 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 v} {s : } {M : Type u_1} [inst : ] (f : αM) (p : MProp) (hom : (a b : M) → p ap bp (a * b)) (unit : p 1) (base : (x : α) → x sp (f x)) :
p (Finset.prod s 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 v} {s : } {M : Type u_1} [inst : ] (f : αM) (p : MProp) (hom : (a b : M) → p ap bp (a + b)) (nonempty : ) (base : (x : α) → x sp (f x)) :
p (Finset.sum s 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 v} {s : } {M : Type u_1} [inst : ] (f : αM) (p : MProp) (hom : (a b : M) → p ap bp (a * b)) (nonempty : ) (base : (x : α) → x sp (f x)) :
p (Finset.prod s 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} [inst : ] (f : β) (s : β) (base : s 0 = 0) (step : ∀ (n : ), s (n + 1) = s n + f n) (n : ) :
(Finset.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} [inst : ] (f : β) (s : β) (base : s 0 = 1) (step : ∀ (n : ), s (n + 1) = s n * f n) (n : ) :
(Finset.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_1} [inst : ] (f : M) (n : ) :
(Finset.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_1} [inst : ] (f : M) (n : ) :
(Finset.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_1} [inst : ] (f : M) (n : ) :
(Finset.sum () fun i => f i - f (i + 1)) = f 0 - f n
theorem Finset.prod_range_div' {M : Type u_1} [inst : ] (f : M) (n : ) :
(Finset.prod () fun i => f i / f (i + 1)) = f 0 / f n
theorem Finset.eq_sum_range_sub {M : Type u_1} [inst : ] (f : M) (n : ) :
f n = f 0 + Finset.sum () fun i => f (i + 1) - f i
theorem Finset.eq_prod_range_div {M : Type u_1} [inst : ] (f : M) (n : ) :
f n = f 0 * Finset.prod () fun i => f (i + 1) / f i
theorem Finset.eq_sum_range_sub' {M : Type u_1} [inst : ] (f : M) (n : ) :
f n = Finset.sum (Finset.range (n + 1)) fun i => if i = 0 then f 0 else f i - f (i - 1)
theorem Finset.eq_prod_range_div' {M : Type u_1} [inst : ] (f : M) (n : ) :
f n = Finset.prod (Finset.range (n + 1)) fun i => if i = 0 then f 0 else f i / f (i - 1)
theorem Finset.sum_range_tsub {α : Type v} [inst : ] [inst : Sub α] [inst : ] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {f : α} (h : ) (n : ) :
(Finset.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} {α : Type v} {s : } [inst : ] (b : β) :
(Finset.sum s fun _x => b) = b
@[simp]
theorem Finset.prod_const {β : Type u} {α : Type v} {s : } [inst : ] (b : β) :
(Finset.prod s fun _x => b) = b ^
theorem Finset.sum_eq_card_nsmul {β : Type u} {α : Type v} {s : } {f : αβ} [inst : ] {b : β} (hf : ∀ (a : α), a sf a = b) :
(Finset.sum s fun a => f a) = b
theorem Finset.prod_eq_pow_card {β : Type u} {α : Type v} {s : } {f : αβ} [inst : ] {b : β} (hf : ∀ (a : α), a sf a = b) :
(Finset.prod s fun a => f a) = b ^
theorem Finset.nsmul_eq_sum_const {β : Type u} [inst : ] (b : β) (n : ) :
n b = Finset.sum () fun _k => b
theorem Finset.pow_eq_prod_const {β : Type u} [inst : ] (b : β) (n : ) :
b ^ n = Finset.prod () fun _k => b
theorem Finset.sum_nsmul {β : Type u} {α : Type v} [inst : ] (s : ) (n : ) (f : αβ) :
(Finset.sum s fun x => n f x) = n Finset.sum s fun x => f x
theorem Finset.prod_pow {β : Type u} {α : Type v} [inst : ] (s : ) (n : ) (f : αβ) :
(Finset.prod s fun x => f x ^ n) = (Finset.prod s fun x => f x) ^ n
theorem Finset.sum_flip {β : Type u} [inst : ] {n : } (f : β) :
(Finset.sum (Finset.range (n + 1)) fun r => f (n - r)) = Finset.sum (Finset.range (n + 1)) fun k => f k
theorem Finset.prod_flip {β : Type u} [inst : ] {n : } (f : β) :
(Finset.prod (Finset.range (n + 1)) fun r => f (n - r)) = Finset.prod (Finset.range (n + 1)) fun k => f k
theorem Finset.sum_involution {β : Type u} {α : Type v} [inst : ] {s : } {f : αβ} (g : (a : α) → a sα) :
(∀ (a : α) (ha : a s), f a + f (g a ha) = 0) → (∀ (a : α) (ha : a s), f a 0g a ha a) → ∀ (g_mem : ∀ (a : α) (ha : a s), g a ha s), (∀ (a : α) (ha : a s), g (g a ha) (_ : g a ha s) = a) → (Finset.sum s fun x => f x) = 0
abbrev Finset.sum_involution.match_1 {α : Type u_1} (s : ) (motive : ) :
(x : ) → ((x : α) → (hx : x s) → motive (_ : x, x s)) → motive x
Equations
theorem Finset.prod_involution {β : Type u} {α : Type v} [inst : ] {s : } {f : αβ} (g : (a : α) → a sα) :
(∀ (a : α) (ha : a s), f a * f (g a ha) = 1) → (∀ (a : α) (ha : a s), f a 1g a ha a) → ∀ (g_mem : ∀ (a : α) (ha : a s), g a ha s), (∀ (a : α) (ha : a s), g (g a ha) (_ : g a ha s) = a) → (Finset.prod s fun x => f x) = 1
theorem Finset.sum_comp {β : Type u} {α : Type v} {γ : Type w} {s : } [inst : ] [inst : ] (f : γβ) (g : αγ) :
(Finset.sum s fun a => f (g a)) = Finset.sum () fun b => Finset.card (Finset.filter (fun a => g a = b) s) 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} {α : Type v} {γ : Type w} {s : } [inst : ] [inst : ] (f : γβ) (g : αγ) :
(Finset.prod s fun a => f (g a)) = Finset.prod () fun b => f b ^ Finset.card (Finset.filter (fun a => g a = b) s)

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} {α : Type v} [inst : ] [inst : ] (s : ) (t : ) (f : αβ) (g : αβ) :
(Finset.sum s fun x => Finset.piecewise t f g x) = (Finset.sum (s t) fun x => f x) + Finset.sum (s \ t) fun x => g x
theorem Finset.prod_piecewise {β : Type u} {α : Type v} [inst : ] [inst : ] (s : ) (t : ) (f : αβ) (g : αβ) :
(Finset.prod s fun x => Finset.piecewise t f g x) = (Finset.prod (s t) fun x => f x) * Finset.prod (s \ t) fun x => g x
theorem Finset.sum_inter_add_sum_diff {β : Type u} {α : Type v} [inst : ] [inst : ] (s : ) (t : ) (f : αβ) :
((Finset.sum (s t) fun x => f x) + Finset.sum (s \ t) fun x => f x) = Finset.sum s fun x => f x
theorem Finset.prod_inter_mul_prod_diff {β : Type u} {α : Type v} [inst : ] [inst : ] (s : ) (t : ) (f : αβ) :
((Finset.prod (s t) fun x => f x) * Finset.prod (s \ t) fun x => f x) = Finset.prod s fun x => f x
theorem Finset.sum_eq_add_sum_diff_singleton {β : Type u} {α : Type v} [inst : ] [inst : ] {s : } {i : α} (h : i s) (f : αβ) :
(Finset.sum s fun x => f x) = f i + Finset.sum (s \ {i}) fun x => f x
theorem Finset.prod_eq_mul_prod_diff_singleton {β : Type u} {α : Type v} [inst : ] [inst : ] {s : } {i : α} (h : i s) (f : αβ) :
(Finset.prod s fun x => f x) = f i * Finset.prod (s \ {i}) fun x => f x
theorem Finset.sum_eq_sum_diff_singleton_add {β : Type u} {α : Type v} [inst : ] [inst : ] {s : } {i : α} (h : i s) (f : αβ) :
(Finset.sum s fun x => f x) = (Finset.sum (s \ {i}) fun x => f x) + f i
theorem Finset.prod_eq_prod_diff_singleton_mul {β : Type u} {α : Type v} [inst : ] [inst : ] {s : } {i : α} (h : i s) (f : αβ) :
(Finset.prod s fun x => f x) = (Finset.prod (s \ {i}) fun x => f x) * f i
theorem Fintype.sum_eq_add_sum_compl {β : Type u} {α : Type v} [inst : ] [inst : ] [inst : ] (a : α) (f : αβ) :
(Finset.sum Finset.univ fun i => f i) = f a + Finset.sum ({a}) fun i => f i
theorem Fintype.prod_eq_mul_prod_compl {β : Type u} {α : Type v} [inst : ] [inst : ] [inst : ] (a : α) (f : αβ) :
(Finset.prod Finset.univ fun i => f i) = f a * Finset.prod ({a}) fun i => f i
theorem Fintype.sum_eq_sum_compl_add {β : Type u} {α : Type v} [inst : ] [inst : ] [inst : ] (a : α) (f : αβ) :
(Finset.sum Finset.univ fun i => f i) = (Finset.sum ({a}) fun i => f i) + f a
theorem Fintype.prod_eq_prod_compl_mul {β : Type u} {α : Type v} [inst : ] [inst : ] [inst : ] (a : α) (f : αβ) :
(Finset.prod Finset.univ fun i => f i) = (Finset.prod ({a}) fun i => f i) * f a
theorem Finset.dvd_prod_of_mem {β : Type u} {α : Type v} [inst : ] (f : αβ) {a : α} {s : } (ha : a s) :
f a Finset.prod s fun i => f i
theorem Finset.sum_partition {β : Type u} {α : Type v} {s : } {f : αβ} [inst : ] (R : ) [inst : DecidableRel Setoid.r] :
(Finset.sum s fun x => f x) = Finset.sum (Finset.image Quotient.mk'' s) fun xbar => Finset.sum (Finset.filter (fun x => = xbar) s) 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} {α : Type v} {s : } {f : αβ} [inst : ] (R : ) [inst : DecidableRel Setoid.r] :
(Finset.prod s fun x => f x) = Finset.prod (Finset.image Quotient.mk'' s) fun xbar => Finset.prod (Finset.filter (fun x => = xbar) s) 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} {α : Type v} {s : } {f : αβ} [inst : ] (R : ) [inst : DecidableRel Setoid.r] (h : ∀ (x : α), x s(Finset.sum (Finset.filter (fun y => y x) s) fun a => f a) = 0) :
(Finset.sum s 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} {α : Type v} {s : } {f : αβ} [inst : ] (R : ) [inst : DecidableRel Setoid.r] (h : ∀ (x : α), x s(Finset.prod (Finset.filter (fun y => y x) s) fun a => f a) = 1) :
(Finset.prod s 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} {α : Type v} [inst : ] [inst : ] {s : } {i : α} (h : ¬i s) (f : αβ) (b : β) :
(Finset.sum s fun x => Function.update f i b x) = Finset.sum s fun x => f x
theorem Finset.prod_update_of_not_mem {β : Type u} {α : Type v} [inst : ] [inst : ] {s : } {i : α} (h : ¬i s) (f : αβ) (b : β) :
(Finset.prod s fun x => Function.update f i b x) = Finset.prod s fun x => f x
theorem Finset.sum_update_of_mem {β : Type u} {α : Type v} [inst : ] [inst : ] {s : } {i : α} (h : i s) (f : αβ) (b : β) :
(Finset.sum s fun x => Function.update f i b x) = b + Finset.sum (s \ {i}) fun x => f x
theorem Finset.prod_update_of_mem {β : Type u} {α : Type v} [inst : ] [inst : ] {s : } {i : α} (h : i s) (f : αβ) (b : β) :
(Finset.prod s fun x => Function.update f i b x) = b * Finset.prod (s \ {i}) fun x => f x
theorem Finset.eq_of_card_le_one_of_sum_eq {β : Type u} {α : Type v} [inst : ] {s : } (hc : 1) {f : αβ} {b : β} (h : (Finset.sum s fun x => f x) = b) (x : α) :
x sf 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} {α : Type v} [inst : ] {s : } (hc : 1) {f : αβ} {b : β} (h : (Finset.prod s fun x => f x) = b) (x : α) :
x sf 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} {α : Type v} [inst : ] [inst : ] (s : ) (f : αβ) {a : α} (h : a s) :
(f a + Finset.sum () fun x => f x) = Finset.sum s 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} {α : Type v} [inst : ] [inst : ] (s : ) (f : αβ) {a : α} (h : a s) :
(f a * Finset.prod () fun x => f x) = Finset.prod s 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} {α : Type v} [inst : ] [inst : ] (s : ) (f : αβ) {a : α} (h : a s) :
(Finset.sum () fun x => f x) + f a = Finset.sum s fun x => f x

A variant of Finset.add_sum_erase with the addition swapped.

theorem Finset.prod_erase_mul {β : Type u} {α : Type v} [inst : ] [inst : ] (s : ) (f : αβ) {a : α} (h : a s) :
(Finset.prod () fun x => f x) * f a = Finset.prod s fun x => f x

A variant of Finset.mul_prod_erase with the multiplication swapped.

theorem Finset.sum_erase {β : Type u} {α : Type v} [inst : ] [inst : ] (s : ) {f : αβ} {a : α} (h : f a = 0) :
(Finset.sum () fun x => f x) = Finset.sum s 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} {α : Type v} [inst : ] [inst : ] (s : ) {f : αβ} {a : α} (h : f a = 1) :
(Finset.prod () fun x => f x) = Finset.prod s 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} {α : Type v} {s : } [inst : ] {f : αProp} [inst : ] (hf : Set.PairwiseDisjoint (s) f) (a : β) :
(Finset.sum s fun i => if f i then a else 0) = if i, i s f i then a else 0

See also Finset.sum_boole.

theorem Finset.prod_ite_one {β : Type u} {α : Type v} {s : } [inst : ] {f : αProp} [inst : ] (hf : Set.PairwiseDisjoint (s) f) (a : β) :
(Finset.prod s fun i => if f i then a else 1) = if i, i s f i then a else 1

See also Finset.prod_boole.