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.

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 : AddCommMonoid β] (s : Finset α) (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 : CommMonoid β] (s : Finset α) (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 : AddCommMonoid β] (s : Multiset α) (hs : Multiset.Nodup s) (f : αβ) :
Finset.sum { val := s, nodup := hs } f = Multiset.sum (Multiset.map f s)
@[simp]
theorem Finset.prod_mk {β : Type u} {α : Type v} [inst : CommMonoid β] (s : Multiset α) (hs : Multiset.Nodup s) (f : αβ) :
Finset.prod { val := s, nodup := hs } f = Multiset.prod (Multiset.map f s)
@[simp]
theorem Finset.sum_val {α : Type v} [inst : AddCommMonoid α] (s : Finset α) :
@[simp]
theorem Finset.prod_val {α : Type v} [inst : CommMonoid α] (s : Finset α) :

∑ 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 : AddCommMonoid β] (s : Finset α) (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 : CommMonoid β] (s : Finset α) (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 : AddCommMonoid β] (s : Finset α) (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 : CommMonoid β] (s : Finset α) (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 α) :
(Finset.sum s fun x => {x}) = s.val
theorem map_sum {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] [inst : AddCommMonoid γ] {G : Type u_1} [inst : AddMonoidHomClass G β γ] (g : G) (f : αβ) (s : Finset α) :
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 : CommMonoid β] [inst : CommMonoid γ] {G : Type u_1} [inst : MonoidHomClass G β γ] (g : G) (f : αβ) (s : Finset α) :
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 : AddCommMonoid β] [inst : AddCommMonoid γ] (g : β →+ γ) (f : αβ) (s : Finset α) :
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 : CommMonoid β] [inst : CommMonoid γ] (g : β →* γ) (f : αβ) (s : Finset α) :
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 : AddCommMonoid β] [inst : AddCommMonoid γ] (g : β ≃+ γ) (f : αβ) (s : Finset α) :
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 : CommMonoid β] [inst : CommMonoid γ] (g : β ≃* γ) (f : αβ) (s : Finset α) :
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 : Semiring β] [inst : Semiring γ] (f : β →+* γ) (l : List β) :
f (List.prod l) = List.prod (List.map (f) l)
theorem RingHom.map_list_sum {β : Type u} {γ : Type w} [inst : NonAssocSemiring β] [inst : NonAssocSemiring γ] (f : β →+* γ) (l : List β) :
f (List.sum l) = List.sum (List.map (f) l)
theorem RingHom.unop_map_list_prod {β : Type u} {γ : Type w} [inst : Semiring β] [inst : Semiring γ] (f : β →+* γᵐᵒᵖ) (l : List β) :
(f (List.prod l)).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 : CommSemiring β] [inst : CommSemiring γ] (f : β →+* γ) (s : Multiset β) :
theorem RingHom.map_multiset_sum {β : Type u} {γ : Type w} [inst : NonAssocSemiring β] [inst : NonAssocSemiring γ] (f : β →+* γ) (s : Multiset β) :
theorem RingHom.map_prod {β : Type u} {α : Type v} {γ : Type w} [inst : CommSemiring β] [inst : CommSemiring γ] (g : β →+* γ) (f : αβ) (s : Finset α) :
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 : NonAssocSemiring β] [inst : NonAssocSemiring γ] (g : β →+* γ) (f : αβ) (s : Finset α) :
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 : AddZeroClass β] [inst : AddCommMonoid γ] (f : αβ →+ γ) (s : Finset α) :
↑(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 : MulOneClass β] [inst : CommMonoid γ] (f : αβ →* γ) (s : Finset α) :
↑(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 : AddZeroClass β] [inst : AddCommMonoid γ] (f : αβ →+ γ) (s : Finset α) (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 : MulOneClass β] [inst : CommMonoid γ] (f : αβ →* γ) (s : Finset α) (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 : AddCommMonoid β] :
(Finset.sum fun x => f x) = 0
@[simp]
theorem Finset.prod_empty {β : Type u} {α : Type v} {f : αβ} [inst : CommMonoid β] :
(Finset.prod fun x => f x) = 1
theorem Finset.sum_of_empty {β : Type u} {α : Type v} {f : αβ} [inst : AddCommMonoid β] [inst : IsEmpty α] (s : Finset α) :
(Finset.sum s fun i => f i) = 0
theorem Finset.prod_of_empty {β : Type u} {α : Type v} {f : αβ} [inst : CommMonoid β] [inst : IsEmpty α] (s : Finset α) :
(Finset.prod s fun i => f i) = 1
@[simp]
theorem Finset.sum_cons {β : Type u} {α : Type v} {s : Finset α} {a : α} {f : αβ} [inst : AddCommMonoid β] (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 : Finset α} {a : α} {f : αβ} [inst : CommMonoid β] (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 : Finset α} {a : α} {f : αβ} [inst : AddCommMonoid β] [inst : DecidableEq α] :
¬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 : Finset α} {a : α} {f : αβ} [inst : CommMonoid β] [inst : DecidableEq α] :
¬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 : Finset α} {a : α} {f : αβ} [inst : AddCommMonoid β] [inst : DecidableEq α] (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 : Finset α} {a : α} {f : αβ} [inst : CommMonoid β] [inst : DecidableEq α] (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 : Finset α} {a : α} {f : αβ} [inst : AddCommMonoid β] [inst : DecidableEq α] (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 : Finset α} {a : α} {f : αβ} [inst : CommMonoid β] [inst : DecidableEq α] (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 : AddCommMonoid β] :
(Finset.sum {a} fun x => f x) = f a
@[simp]
theorem Finset.prod_singleton {β : Type u} {α : Type v} {a : α} {f : αβ} [inst : CommMonoid β] :
(Finset.prod {a} fun x => f x) = f a
theorem Finset.sum_pair {β : Type u} {α : Type v} {f : αβ} [inst : AddCommMonoid β] [inst : DecidableEq α] {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 : CommMonoid β] [inst : DecidableEq α] {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 : Finset α} [inst : AddCommMonoid β] :
(Finset.sum s fun _x => 0) = 0
@[simp]
theorem Finset.prod_const_one {β : Type u} {α : Type v} {s : Finset α} [inst : CommMonoid β] :
(Finset.prod s fun _x => 1) = 1
@[simp]
theorem Finset.sum_image {β : Type u} {α : Type v} {γ : Type w} {f : αβ} [inst : AddCommMonoid β] [inst : DecidableEq α] {s : Finset γ} {g : γα} :
(∀ (x : γ), x s∀ (y : γ), y sg x = g yx = y) → (Finset.sum (Finset.image g s) 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 : CommMonoid β] [inst : DecidableEq α] {s : Finset γ} {g : γα} :
(∀ (x : γ), x s∀ (y : γ), y sg x = g yx = y) → (Finset.prod (Finset.image g s) fun x => f x) = Finset.prod s fun x => f (g x)
@[simp]
theorem Finset.sum_map {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] (s : Finset α) (e : α γ) (f : γβ) :
(Finset.sum (Finset.map e s) fun x => f x) = Finset.sum s fun x => f (e x)
@[simp]
theorem Finset.prod_map {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] (s : Finset α) (e : α γ) (f : γβ) :
(Finset.prod (Finset.map e s) fun x => f x) = Finset.prod s fun x => f (e x)
theorem Finset.sum_congr {β : Type u} {α : Type v} {s₁ : Finset α} {s₂ : Finset α} {f : αβ} {g : αβ} [inst : AddCommMonoid β] (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₁ : Finset α} {s₂ : Finset α} {f : αβ} {g : αβ} [inst : CommMonoid β] (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₁ : Finset α} {s₂ : Finset α} {f : αβ} [inst : AddCommMonoid β] (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₁ : Finset α} {s₂ : Finset α} {f : αβ} [inst : CommMonoid β] (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 : AddCommMonoid β] (s : Finset ι) (t : ιFinset α) (h : Set.PairwiseDisjoint (s) t) :
(Finset.sum (Finset.disjUnionᵢ s t h) 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 : CommMonoid β] (s : Finset ι) (t : ιFinset α) (h : Set.PairwiseDisjoint (s) t) :
(Finset.prod (Finset.disjUnionᵢ s t h) 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₁ : Finset α} {s₂ : Finset α} {f : αβ} [inst : AddCommMonoid β] [inst : DecidableEq α] :
((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₁ : Finset α} {s₂ : Finset α} {f : αβ} [inst : CommMonoid β] [inst : DecidableEq α] :
((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₁ : Finset α} {s₂ : Finset α} {f : αβ} [inst : AddCommMonoid β] [inst : DecidableEq α] (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₁ : Finset α} {s₂ : Finset α} {f : αβ} [inst : CommMonoid β] [inst : DecidableEq α] (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 : AddCommMonoid β] (s : Finset α) (p : αProp) [inst : DecidablePred p] [inst : (x : α) → Decidable ¬p x] (f : αβ) :
((Finset.sum (Finset.filter p s) 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 : CommMonoid β] (s : Finset α) (p : αProp) [inst : DecidablePred p] [inst : (x : α) → Decidable ¬p x] (f : αβ) :
((Finset.prod (Finset.filter p s) 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 : AddCommMonoid β] (s : Finset α) (f : αβ) :
@[simp]
theorem Finset.prod_to_list {β : Type u} {α : Type v} [inst : CommMonoid β] (s : Finset α) (f : αβ) :
theorem Equiv.Perm.sum_comp {β : Type u} {α : Type v} [inst : AddCommMonoid β] (σ : Equiv.Perm α) (s : Finset α) (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 : CommMonoid β] (σ : Equiv.Perm α) (s : Finset α) (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 : AddCommMonoid β] (σ : Equiv.Perm α) (s : Finset α) (f : ααβ) (hs : { a | σ a a } s) :
(Finset.sum s fun x => f (σ x) x) = Finset.sum s fun x => f x (↑(Equiv.symm σ) x)
theorem Equiv.Perm.prod_comp' {β : Type u} {α : Type v} [inst : CommMonoid β] (σ : Equiv.Perm α) (s : Finset α) (f : ααβ) (hs : { a | σ a a } s) :
(Finset.prod s fun x => f (σ x) x) = Finset.prod s fun x => f x (↑(Equiv.symm σ) x)
theorem IsCompl.sum_add_sum {β : Type u} {α : Type v} [inst : Fintype α] [inst : AddCommMonoid β] {s : Finset α} {t : Finset α} (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 : Fintype α] [inst : CommMonoid β] {s : Finset α} {t : Finset α} (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 : AddCommMonoid β] [inst : Fintype α] [inst : DecidableEq α] (s : Finset α) (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 : CommMonoid β] [inst : Fintype α] [inst : DecidableEq α] (s : Finset α) (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 : AddCommMonoid β] [inst : Fintype α] [inst : DecidableEq α] (s : Finset α) (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 : CommMonoid β] [inst : Fintype α] [inst : DecidableEq α] (s : Finset α) (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₁ : Finset α} {s₂ : Finset α} {f : αβ} [inst : AddCommMonoid β] [inst : DecidableEq α] (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₁ : Finset α} {s₂ : Finset α} {f : αβ} [inst : CommMonoid β] [inst : DecidableEq α] (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 : AddCommMonoid β] (s : Finset α) (t : Finset γ) (f : α γβ) :
(Finset.sum (Finset.disjSum s t) fun x => f x) = (Finset.sum s fun x => f (Sum.inl x)) + Finset.sum t fun x => f (Sum.inr x)
@[simp]
theorem Finset.prod_disj_sum {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] (s : Finset α) (t : Finset γ) (f : α γβ) :
(Finset.prod (Finset.disjSum s t) fun x => f x) = (Finset.prod s fun x => f (Sum.inl x)) * Finset.prod t fun x => f (Sum.inr x)
theorem Finset.sum_sum_elim {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] (s : Finset α) (t : Finset γ) (f : αβ) (g : γβ) :
(Finset.sum (Finset.disjSum s t) 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 : CommMonoid β] (s : Finset α) (t : Finset γ) (f : αβ) (g : γβ) :
(Finset.prod (Finset.disjSum s t) 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 : AddCommMonoid β] [inst : DecidableEq α] {s : Finset γ} {t : γFinset α} (hs : Set.PairwiseDisjoint (s) t) :
(Finset.sum (Finset.bunionᵢ s t) 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 : CommMonoid β] [inst : DecidableEq α] {s : Finset γ} {t : γFinset α} (hs : Set.PairwiseDisjoint (s) t) :
(Finset.prod (Finset.bunionᵢ s t) 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 : AddCommMonoid β] {σ : αType u_1} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : Sigma σβ) :
(Finset.sum (Finset.sigma s t) 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 : CommMonoid β] {σ : αType u_1} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : Sigma σβ) :
(Finset.prod (Finset.sigma s t) 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 : AddCommMonoid β] {σ : αType u_1} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : (a : α) → σ aβ) :
(Finset.sum s fun a => Finset.sum (t a) fun s => f a s) = Finset.sum (Finset.sigma s t) fun x => f x.fst x.snd
theorem Finset.prod_sigma' {β : Type u} {α : Type v} [inst : CommMonoid β] {σ : αType u_1} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : (a : α) → σ aβ) :
(Finset.prod s fun a => Finset.prod (t a) fun s => f a s) = Finset.prod (Finset.sigma s t) fun x => f x.fst x.snd
theorem Finset.sum_bij {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] {s : Finset α} {t : Finset γ} {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 : CommMonoid β] {s : Finset α} {t : Finset γ} {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 : AddCommMonoid β] {s : Finset α} {t : Finset γ} {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 : CommMonoid β] {s : Finset α} {t : Finset γ} {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 : AddCommMonoid β] {ι' : Type u_1} [inst : DecidableEq ι] (e : ι ι') (f : ι'β) {s' : Finset ι'} {s : Finset ι} (h : s = Finset.image (↑(Equiv.symm e)) 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 : CommMonoid β] {ι' : Type u_1} [inst : DecidableEq ι] (e : ι ι') (f : ι'β) {s' : Finset ι'} {s : Finset ι} (h : s = Finset.image (↑(Equiv.symm e)) 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 : AddCommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γFinset α) (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 : CommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γFinset α) (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 : AddCommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γFinset α) (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 : CommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γFinset α) (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 : AddCommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γFinset α) (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 : CommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γFinset α) (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 : AddCommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γFinset α) (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 : CommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γFinset α) (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 : AddCommMonoid β] [inst : DecidableEq γ] {s : Finset α} {t : Finset γ} {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 : CommMonoid β] [inst : DecidableEq γ] {s : Finset α} {t : Finset γ} {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 : Finset γ} {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 : AddCommMonoid β] [inst : DecidableEq α] {s : Finset γ} {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 (Finset.image g s) fun x => f x) = Finset.sum s fun x => h x
theorem Finset.prod_image' {β : Type u} {α : Type v} {γ : Type w} {f : αβ} [inst : CommMonoid β] [inst : DecidableEq α] {s : Finset γ} {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 (Finset.image g s) fun x => f x) = Finset.prod s fun x => h x
theorem Finset.sum_add_distrib {β : Type u} {α : Type v} {s : Finset α} {f : αβ} {g : αβ} [inst : AddCommMonoid β] :
(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 : Finset α} {f : αβ} {g : αβ} [inst : CommMonoid β] :
(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 : AddCommMonoid β] {s : Finset γ} {t : Finset α} {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 : CommMonoid β] {s : Finset γ} {t : Finset α} {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 : AddCommMonoid β] {s : Finset γ} {t : Finset α} {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 : CommMonoid β] {s : Finset γ} {t : Finset α} {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 : AddCommMonoid β] {s : Finset γ} {t : Finset α} {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 : CommMonoid β] {s : Finset γ} {t : Finset α} {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 : AddCommMonoid β] {s : Finset γ} {t : Finset α} {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 : CommMonoid β] {s : Finset γ} {t : Finset α} {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 : AddCommMonoid β] {s : Finset γ} {t : γFinset α} {t' : Finset α} {s' : αFinset γ} (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 : CommMonoid β] {s : Finset γ} {t : γFinset α} {t' : Finset α} {s' : αFinset γ} (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 : AddCommMonoid β] {s : Finset γ} {t : Finset α} {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 : CommMonoid β] {s : Finset γ} {t : Finset α} {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 : AddCommMonoid β] [inst : AddCommMonoid γ] {r : βγProp} {f : αβ} {g : αγ} {s : Finset α} (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 : CommMonoid β] [inst : CommMonoid γ] {r : βγProp} {f : αβ} {g : αγ} {s : Finset α} (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 : AddCommMonoid β] {f : αβ} {s : Finset α} (h : ∀ (x : α), x sf x = 0) :
(Finset.sum s fun x => f x) = 0
theorem Finset.prod_eq_one {β : Type u} {α : Type v} [inst : CommMonoid β] {f : αβ} {s : Finset α} (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₁ : Finset α} {s₂ : Finset α} {f : αβ} {g : αβ} [inst : AddCommMonoid β] [inst : DecidableEq α] (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₁ : Finset α} {s₂ : Finset α} {f : αβ} {g : αβ} [inst : CommMonoid β] [inst : DecidableEq α] (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₁ : Finset α} {s₂ : Finset α} {f : αβ} [inst : AddCommMonoid β] (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₁ : Finset α} {s₂ : Finset α} {f : αβ} [inst : CommMonoid β] (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 : Finset α} {f : αβ} [inst : AddCommMonoid β] {p : αProp} [inst : DecidablePred p] (hp : (x : α) → x sf x 0p x) :
(Finset.sum (Finset.filter p s) fun x => f x) = Finset.sum s fun x => f x
theorem Finset.prod_filter_of_ne {β : Type u} {α : Type v} {s : Finset α} {f : αβ} [inst : CommMonoid β] {p : αProp} [inst : DecidablePred p] (hp : (x : α) → x sf x 1p x) :
(Finset.prod (Finset.filter p s) fun x => f x) = Finset.prod s fun x => f x
theorem Finset.sum_filter_ne_zero {β : Type u} {α : Type v} {s : Finset α} {f : αβ} [inst : AddCommMonoid β] [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 : Finset α} {f : αβ} [inst : CommMonoid β] [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 : Finset α} [inst : AddCommMonoid β] (p : αProp) [inst : DecidablePred p] (f : αβ) :
(Finset.sum (Finset.filter p s) 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 : Finset α} [inst : CommMonoid β] (p : αProp) [inst : DecidablePred p] (f : αβ) :
(Finset.prod (Finset.filter p s) 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 : AddCommMonoid β] {s : Finset α} {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 : CommMonoid β] {s : Finset α} {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 : AddCommMonoid β] {s : Finset α} {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 : Finset α} (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 : CommMonoid β] {s : Finset α} {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 : AddCommMonoid β] {s : Finset α} {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 : CommMonoid β] {s : Finset α} {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 : AddCommMonoid β] {s : Finset α} {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 : CommMonoid β] {s : Finset α} {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 : Finset α} [inst : AddCommMonoid β] {f : αβ} :
(Finset.sum (Finset.attach s) fun x => f x) = Finset.sum s fun x => f x
theorem Finset.prod_attach {β : Type u} {α : Type v} {s : Finset α} [inst : CommMonoid β] {f : αβ} :
(Finset.prod (Finset.attach s) fun x => f x) = Finset.prod s fun x => f x
@[simp]
theorem Finset.sum_subtype_eq_sum_filter {β : Type u} {α : Type v} {s : Finset α} [inst : AddCommMonoid β] (f : αβ) {p : αProp} [inst : DecidablePred p] :
(Finset.sum (Finset.subtype p s) fun x => f x) = Finset.sum (Finset.filter p s) 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 : Finset α} [inst : CommMonoid β] (f : αβ) {p : αProp} [inst : DecidablePred p] :
(Finset.prod (Finset.subtype p s) fun x => f x) = Finset.prod (Finset.filter p s) 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 : Finset α} [inst : AddCommMonoid β] (f : αβ) {p : αProp} [inst : DecidablePred p] (h : (x : α) → x sp x) :
(Finset.sum (Finset.subtype p s) 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 : Finset α} [inst : CommMonoid β] (f : αβ) {p : αProp} [inst : DecidablePred p] (h : (x : α) → x sp x) :
(Finset.prod (Finset.subtype p s) 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 : AddCommMonoid β] {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 : CommMonoid β] {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 : Finset α) [inst : AddCommMonoid β] (f : { x // x s }β) :
(Finset.sum Finset.univ fun i => f i) = Finset.sum (Finset.attach s) fun i => f i
theorem Finset.prod_coe_sort_eq_attach {β : Type u} {α : Type v} (s : Finset α) [inst : CommMonoid β] (f : { x // x s }β) :
(Finset.prod Finset.univ fun i => f i) = Finset.prod (Finset.attach s) fun i => f i
theorem Finset.sum_coe_sort {β : Type u} {α : Type v} (s : Finset α) (f : αβ) [inst : AddCommMonoid β] :
(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 : Finset α) (f : αβ) [inst : CommMonoid β] :
(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 : AddCommMonoid β] (f : αβ) (s : Finset α) :
(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 : CommMonoid β] (f : αβ) (s : Finset α) :
(Finset.prod Finset.univ fun i => f i) = Finset.prod s fun i => f i
theorem Finset.sum_subtype {β : Type u} {α : Type v} [inst : AddCommMonoid β] {p : αProp} {F : Fintype (Subtype p)} (s : Finset α) (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 : CommMonoid β] {p : αProp} {F : Fintype (Subtype p)} (s : Finset α) (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 : AddCommMonoid α] {β : Type u_2} [inst : Fintype β] (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 : Fintype β] (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 : CommMonoid α] {β : Type u_2} [inst : Fintype β] (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 : AddCommMonoid β] {s : Finset α} {p : αProp} {hp : DecidablePred p} [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 (Finset.attach (Finset.filter p s)) 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 : CommMonoid β] {s : Finset α} {p : αProp} {hp : DecidablePred p} [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 (Finset.attach (Finset.filter p s)) 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 : AddCommMonoid β] {s : Finset α} {p : αProp} {_hp : DecidablePred p} (f : αγ) (g : αγ) (h : γβ) :
(Finset.sum s fun x => h (if p x then f x else g x)) = (Finset.sum (Finset.filter p s) 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 : CommMonoid β] {s : Finset α} {p : αProp} {_hp : DecidablePred p} (f : αγ) (g : αγ) (h : γβ) :
(Finset.prod s fun x => h (if p x then f x else g x)) = (Finset.prod (Finset.filter p s) 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 : AddCommMonoid β] {s : Finset α} {p : αProp} {hp : DecidablePred p} (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.attach (Finset.filter p s)) 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 : CommMonoid β] {s : Finset α} {p : αProp} {hp : DecidablePred p} (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.attach (Finset.filter p s)) 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 : AddCommMonoid β] {s : Finset α} {p : αProp} {hp : DecidablePred p} (f : αβ) (g : αβ) :
(Finset.sum s fun x => if p x then f x else g x) = (Finset.sum (Finset.filter p s) 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 : CommMonoid β] {s : Finset α} {p : αProp} {hp : DecidablePred p} (f : αβ) (g : αβ) :
(Finset.prod s fun x => if p x then f x else g x) = (Finset.prod (Finset.filter p s) 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 : Finset α} [inst : AddCommMonoid β] {p : αProp} {hp : DecidablePred p} (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 : Finset α} [inst : CommMonoid β] {p : αProp} {hp : DecidablePred p} (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 : Finset α} [inst : AddCommMonoid β] {p : αProp} {hp : DecidablePred p} (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 : Finset α} [inst : CommMonoid β] {p : αProp} {hp : DecidablePred p} (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 : Finset α} [inst : AddCommMonoid β] {p : αProp} {hp : DecidablePred p} (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 : Finset α} [inst : CommMonoid β] {p : αProp} {hp : DecidablePred p} (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 : Finset α} [inst : AddCommMonoid β] {p : αProp} {hp : DecidablePred p} (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 : Finset α} [inst : CommMonoid β] {p : αProp} {hp : DecidablePred p} (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 : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (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 : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (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 : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (t : Finset α) (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 : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (t : Finset α) (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 : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (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 : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (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 : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (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 : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (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 : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (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 : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (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 : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (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 : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (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 : AddCommMonoid β] (p : Prop) [inst : Decidable p] (s : Finset α) (t : Finset α) (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 : CommMonoid β] (p : Prop) [inst : Decidable p] (s : Finset α) (t : Finset α) (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 : AddCommMonoid β] (p : Prop) [inst : Decidable p] (s : Finset α) (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 : CommMonoid β] (p : Prop) [inst : Decidable p] (s : Finset α) (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 : AddCommMonoid β] (p : Prop) [inst : Decidable p] (s : Finset α) (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 : CommMonoid β] (p : Prop) [inst : Decidable p] (s : Finset α) (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 : DecidableEq ι] [inst : AddCommMonoid M] (i : ι) (x : M) (s : Finset ι) :
(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 : DecidableEq ι] [inst : (i : ι) → AddCommMonoid (M i)] (i : ι) (f : (i : ι) → M i) (s : Finset ι) :
(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 : AddCommMonoid β] {s : Finset α} {t : Finset γ} {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 : CommMonoid β] {s : Finset α} {t : Finset γ} {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 : Finset α} [inst : AddCommMonoid β] {p : αProp} {hp : DecidablePred p} (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 : Finset α} [inst : CommMonoid β] {p : αProp} {hp : DecidablePred p} (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 : Finset α} [inst : AddCommMonoid β] {p : αProp} {hp : DecidablePred p} (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 : Finset α} [inst : CommMonoid β] {p : αProp} {hp : DecidablePred p} (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 : Finset α} {f : αβ} [inst : AddCommMonoid β] (h : (Finset.sum s fun x => f x) 0) :
theorem Finset.nonempty_of_prod_ne_one {β : Type u} {α : Type v} {s : Finset α} {f : αβ} [inst : CommMonoid β] (h : (Finset.prod s fun x => f x) 1) :
theorem Finset.exists_ne_zero_of_sum_ne_zero {β : Type u} {α : Type v} {s : Finset α} {f : αβ} [inst : AddCommMonoid β] (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 : Finset α} {f : αβ} [inst : CommMonoid β] (h : (Finset.prod s fun x => f x) 1) :
a, a s f a 1
theorem Finset.sum_range_succ_comm {β : Type u} [inst : AddCommMonoid β] (f : β) (n : ) :
(Finset.sum (Finset.range (n + 1)) fun x => f x) = f n + Finset.sum (Finset.range n) fun x => f x
theorem Finset.prod_range_succ_comm {β : Type u} [inst : CommMonoid β] (f : β) (n : ) :
(Finset.prod (Finset.range (n + 1)) fun x => f x) = f n * Finset.prod (Finset.range n) fun x => f x
theorem Finset.sum_range_succ {β : Type u} [inst : AddCommMonoid β] (f : β) (n : ) :
(Finset.sum (Finset.range (n + 1)) fun x => f x) = (Finset.sum (Finset.range n) fun x => f x) + f n
theorem Finset.prod_range_succ {β : Type u} [inst : CommMonoid β] (f : β) (n : ) :
(Finset.prod (Finset.range (n + 1)) fun x => f x) = (Finset.prod (Finset.range n) fun x => f x) * f n
abbrev Finset.sum_range_succ'.match_1 (motive : Prop) :
(x : ) → (Unitmotive 0) → ((n : ) → motive (Nat.succ n)) → motive x
Equations
theorem Finset.sum_range_succ' {β : Type u} [inst : AddCommMonoid β] (f : β) (n : ) :
(Finset.sum (Finset.range (n + 1)) fun k => f k) = (Finset.sum (Finset.range n) fun k => f (k + 1)) + f 0
theorem Finset.prod_range_succ' {β : Type u} [inst : CommMonoid β] (f : β) (n : ) :
(Finset.prod (Finset.range (n + 1)) fun k => f k) = (Finset.prod (Finset.range n) fun k => f (k + 1)) * f 0
theorem Finset.eventually_constant_sum {β : Type u} [inst : AddCommMonoid β] {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 : CommMonoid β] {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 : AddCommMonoid β] (f : β) (n : ) (m : ) :
(Finset.sum (Finset.range (n + m)) fun x => f x) = (Finset.sum (Finset.range n) fun x => f x) + Finset.sum (Finset.range m) fun x => f (n + x)
theorem Finset.prod_range_add {β : Type u} [inst : CommMonoid β] (f : β) (n : ) (m : ) :
(Finset.prod (Finset.range (n + m)) fun x => f x) = (Finset.prod (Finset.range n) fun x => f x) * Finset.prod (Finset.range m) fun x => f (n + x)
theorem Finset.sum_range_add_sub_sum_range {α : Type u_1} [inst : AddCommGroup α] (f : α) (n : ) (m : ) :
((Finset.sum (Finset.range (n + m)) fun k => f k) - Finset.sum (Finset.range n) fun k => f k) = Finset.sum (Finset.range m) fun k => f (n + k)
theorem Finset.prod_range_add_div_prod_range {α : Type u_1} [inst : CommGroup α] (f : α) (n : ) (m : ) :
((Finset.prod (Finset.range (n + m)) fun k => f k) / Finset.prod (Finset.range n) fun k => f k) = Finset.prod (Finset.range m) fun k => f (n + k)
theorem Finset.sum_range_zero {β : Type u} [inst : AddCommMonoid β] (f : β) :
(Finset.sum (Finset.range 0) fun k => f k) = 0
theorem Finset.prod_range_zero {β : Type u} [inst : CommMonoid β] (f : β) :
(Finset.prod (Finset.range 0) fun k => f k) = 1
theorem Finset.sum_range_one {β : Type u} [inst : AddCommMonoid β] (f : β) :
(Finset.sum (Finset.range 1) fun k => f k) = f 0
theorem Finset.prod_range_one {β : Type u} [inst : CommMonoid β] (f : β) :
(Finset.prod (Finset.range 1) fun k => f k) = f 0
theorem Finset.sum_list_map_count {α : Type v} [inst : DecidableEq α] (l : List α) {M : Type u_1} [inst : AddCommMonoid M] (f : αM) :
theorem Finset.prod_list_map_count {α : Type v} [inst : DecidableEq α] (l : List α) {M : Type u_1} [inst : CommMonoid M] (f : αM) :
theorem Finset.sum_list_count {α : Type v} [inst : DecidableEq α] [inst : AddCommMonoid α] (s : List α) :
theorem Finset.prod_list_count {α : Type v} [inst : DecidableEq α] [inst : CommMonoid α] (s : List α) :
theorem Finset.sum_list_count_of_subset {α : Type v} [inst : DecidableEq α] [inst : AddCommMonoid α] (m : List α) (s : Finset α) (hs : List.toFinset m s) :
List.sum m = Finset.sum s fun i => List.count i m i
theorem Finset.prod_list_count_of_subset {α : Type v} [inst : DecidableEq α] [inst : CommMonoid α] (m : List α) (s : Finset α) (hs : List.toFinset m s) :
List.prod m = Finset.prod s fun i => i ^ List.count i m
theorem Finset.sum_filter_count_eq_countp {α : Type v} [inst : DecidableEq α] (p : αProp) [inst : DecidablePred p] (l : List α) :
(Finset.sum (Finset.filter p (List.toFinset l)) fun x => List.count x l) = List.countp (fun b => decide (p b)) l
theorem Finset.sum_multiset_map_count {α : Type v} [inst : DecidableEq α] (s : Multiset α) {M : Type u_1} [inst : AddCommMonoid M] (f : αM) :
theorem Finset.prod_multiset_map_count {α : Type v} [inst : DecidableEq α] (s : Multiset α) {M : Type u_1} [inst : CommMonoid M] (f : αM) :
theorem Finset.sum_multiset_count_of_subset {α : Type v} [inst : DecidableEq α] [inst : AddCommMonoid α] (m : Multiset α) (s : Finset α) (hs : Multiset.toFinset m s) :
theorem Finset.prod_multiset_count_of_subset {α : Type v} [inst : DecidableEq α] [inst : CommMonoid α] (m : Multiset α) (s : Finset α) (hs : Multiset.toFinset m s) :
theorem Finset.sum_mem_multiset {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] (m : Multiset α) (f : { x // x m }β) (g : αβ) (hfg : ∀ (x : { x // x m }), f x = g x) :
(Finset.sum Finset.univ fun x => f x) = Finset.sum (Multiset.toFinset m) fun x => g x
theorem Finset.prod_mem_multiset {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] (m : Multiset α) (f : { x // x m }β) (g : αβ) (hfg : ∀ (x : { x // x m }), f x = g x) :
(Finset.prod Finset.univ fun x => f x) = Finset.prod (Multiset.toFinset m) fun x => g x
theorem Finset.sum_induction {α : Type v} {s : Finset α} {M : Type u_1} [inst : AddCommMonoid M] (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 : Finset α} {M : Type u_1} [inst : CommMonoid M] (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 : Finset α} {M : Type u_1} [inst : AddCommMonoid M] (f : αM) (p : MProp) (hom : (a b : M) → p ap bp (a + b)) (nonempty : Finset.Nonempty s) (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 : Finset α} {M : Type u_1} [inst : CommMonoid M] (f : αM) (p : MProp) (hom : (a b : M) → p ap bp (a * b)) (nonempty : Finset.Nonempty s) (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 : AddCommMonoid β] (f : β) (s : β) (base : s 0 = 0) (step : ∀ (n : ), s (n + 1) = s n + f n) (n : ) :
(Finset.sum (Finset.range n) 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 : CommMonoid β] (f : β) (s : β) (base : s 0 = 1) (step : ∀ (n : ), s (n + 1) = s n * f n) (n : ) :
(Finset.prod (Finset.range n) 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 : AddCommGroup M] (f : M) (n : ) :
(Finset.sum (Finset.range n) 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 : CommGroup M] (f : M) (n : ) :
(Finset.prod (Finset.range n) 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 : AddCommGroup M] (f : M) (n : ) :
(Finset.sum (Finset.range n) fun i => f i - f (i + 1)) = f 0 - f n
theorem Finset.prod_range_div' {M : Type u_1} [inst : CommGroup M] (f : M) (n : ) :
(Finset.prod (Finset.range n) fun i => f i / f (i + 1)) = f 0 / f n
theorem Finset.eq_sum_range_sub {M : Type u_1} [inst : AddCommGroup M] (f : M) (n : ) :
f n = f 0 + Finset.sum (Finset.range n) fun i => f (i + 1) - f i
theorem Finset.eq_prod_range_div {M : Type u_1} [inst : CommGroup M] (f : M) (n : ) :
f n = f 0 * Finset.prod (Finset.range n) fun i => f (i + 1) / f i
theorem Finset.eq_sum_range_sub' {M : Type u_1} [inst : AddCommGroup M] (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 : CommGroup M] (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 : CanonicallyOrderedAddMonoid α] [inst : Sub α] [inst : OrderedSub α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {f : α} (h : Monotone f) (n : ) :
(Finset.sum (Finset.range n) 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 : Finset α} [inst : AddCommMonoid β] (b : β) :
(Finset.sum s fun _x => b) = Finset.card s b
@[simp]
theorem Finset.prod_const {β : Type u} {α : Type v} {s : Finset α} [inst : CommMonoid β] (b : β) :
(Finset.prod s fun _x => b) = b ^ Finset.card s
theorem Finset.sum_eq_card_nsmul {β : Type u} {α : Type v} {s : Finset α} {f : αβ} [inst : AddCommMonoid β] {b : β} (hf : ∀ (a : α), a sf a = b) :
(Finset.sum s fun a => f a) = Finset.card s b
theorem Finset.prod_eq_pow_card {β : Type u} {α : Type v} {s : Finset α} {f : αβ} [inst : CommMonoid β] {b : β} (hf : ∀ (a : α), a sf a = b) :
(Finset.prod s fun a => f a) = b ^ Finset.card s
theorem Finset.nsmul_eq_sum_const {β : Type u} [inst : AddCommMonoid β] (b : β) (n : ) :
n b = Finset.sum (Finset.range n) fun _k => b
theorem Finset.pow_eq_prod_const {β : Type u} [inst : CommMonoid β] (b : β) (n : ) :
b ^ n = Finset.prod (Finset.range n) fun _k => b
theorem Finset.sum_nsmul {β : Type u} {α : Type v} [inst : AddCommMonoid β] (s : Finset α) (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 : CommMonoid β] (s : Finset α) (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 : AddCommMonoid β] {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 : CommMonoid β] {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 : 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 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 : Finset α) (motive : Finset.Nonempty sProp) :
(x : Finset.Nonempty s) → ((x : α) → (hx : x s) → motive (_ : x, x s)) → motive x
Equations
theorem Finset.prod_involution {β : Type u} {α : Type v} [inst : 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 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 : Finset α} [inst : AddCommMonoid β] [inst : DecidableEq γ] (f : γβ) (g : αγ) :
(Finset.sum s fun a => f (g a)) = Finset.sum (Finset.image g s) 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 : Finset α} [inst : CommMonoid β] [inst : DecidableEq γ] (f : γβ) (g : αγ) :
(Finset.prod s fun a => f (g a)) = Finset.prod (Finset.image g s) 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 : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (t : Finset α) (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 : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (t : Finset α) (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 : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (t : Finset α) (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 : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (t : Finset α) (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 : AddCommMonoid β] [inst : DecidableEq α] {s : Finset α} {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 : CommMonoid β] [inst : DecidableEq α] {s : Finset α} {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 : AddCommMonoid β] [inst : DecidableEq α] {s : Finset α} {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 : CommMonoid β] [inst : DecidableEq α] {s : Finset α} {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 : AddCommMonoid β] [inst : DecidableEq α] [inst : Fintype α] (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 : CommMonoid β] [inst : DecidableEq α] [inst : Fintype α] (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 : AddCommMonoid β] [inst : DecidableEq α] [inst : Fintype α] (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 : CommMonoid β] [inst : DecidableEq α] [inst : Fintype α] (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 : CommMonoid β] (f : αβ) {a : α} {s : Finset α} (ha : a s) :
f a Finset.prod s fun i => f i
theorem Finset.sum_partition {β : Type u} {α : Type v} {s : Finset α} {f : αβ} [inst : AddCommMonoid β] (R : Setoid α) [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 => Quotient.mk R 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 : Finset α} {f : αβ} [inst : CommMonoid β] (R : Setoid α) [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 => Quotient.mk R 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 : Finset α} {f : αβ} [inst : AddCommMonoid β] (R : Setoid α) [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 : Finset α} {f : αβ} [inst : CommMonoid β] (R : Setoid α) [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 : AddCommMonoid β] [inst : DecidableEq α] {s : Finset α} {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 : CommMonoid β] [inst : DecidableEq α] {s : Finset α} {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 : AddCommMonoid β] [inst : DecidableEq α] {s : Finset α} {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 : CommMonoid β] [inst : DecidableEq α] {s : Finset α} {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 : AddCommMonoid β] {s : Finset α} (hc : Finset.card s 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 : CommMonoid β] {s : Finset α} (hc : Finset.card s 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 : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (f : αβ) {a : α} (h : a s) :
(f a + Finset.sum (Finset.erase s a) 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 : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (f : αβ) {a : α} (h : a s) :
(f a * Finset.prod (Finset.erase s a) 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 : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (f : αβ) {a : α} (h : a s) :
(Finset.sum (Finset.erase s a) 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 : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (f : αβ) {a : α} (h : a s) :
(Finset.prod (Finset.erase s a) 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 : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) {f : αβ} {a : α} (h : f a = 0) :
(Finset.sum (Finset.erase s a) 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 : CommMonoid β] [inst : DecidableEq α] (s : Finset α) {f : αβ} {a : α} (h : f a = 1) :
(Finset.prod (Finset.erase s a) 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 : Finset α} [inst : AddCommMonoid β] {f : αProp} [inst : DecidablePred f] (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 : Finset α} [inst : CommMonoid β] {f : αProp} [inst : DecidablePred f] (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.