# 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} [] (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
Instances For
def Finset.prod {β : Type u} {α : Type v} [] (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
Instances For
@[simp]
theorem Finset.sum_mk {β : Type u} {α : Type v} [] (s : ) (hs : ) (f : αβ) :
Finset.sum { val := s, nodup := hs } f = Multiset.sum ()
@[simp]
theorem Finset.prod_mk {β : Type u} {α : Type v} [] (s : ) (hs : ) (f : αβ) :
Finset.prod { val := s, nodup := hs } f =
@[simp]
theorem Finset.sum_val {α : Type v} [] (s : ) :
@[simp]
theorem Finset.prod_val {α : Type v} [] (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.
Instances For

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

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

∏ x in s, f x is notation for Finset.prod s f. It is the product of f x, where x ranges over the finite set s.

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

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

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

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Finset.sum_eq_multiset_sum {β : Type u} {α : Type v} [] (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} [] (s : ) (f : αβ) :
(Finset.prod s fun (x : α) => f x) = Multiset.prod (Multiset.map f s.val)
@[simp]
theorem Finset.sum_map_val {β : Type u} {α : Type v} [] (s : ) (f : αβ) :
Multiset.sum (Multiset.map f s.val) = Finset.sum s fun (a : α) => f a
@[simp]
theorem Finset.prod_map_val {β : Type u} {α : Type v} [] (s : ) (f : αβ) :
Multiset.prod (Multiset.map f s.val) = Finset.prod s fun (a : α) => f a
theorem Finset.sum_eq_fold {β : Type u} {α : Type v} [] (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} [] (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
@[simp]
theorem map_sum {β : Type u} {α : Type v} {γ : Type w} [] [] {G : Type u_2} [FunLike G β γ] [] (g : G) (f : αβ) (s : ) :
g (Finset.sum s fun (x : α) => f x) = Finset.sum s fun (x : α) => g (f x)
@[simp]
theorem map_prod {β : Type u} {α : Type v} {γ : Type w} [] [] {G : Type u_2} [FunLike G β γ] [] (g : G) (f : αβ) (s : ) :
g (Finset.prod s fun (x : α) => f x) = Finset.prod s fun (x : α) => g (f x)
@[deprecated map_list_prod]
theorem RingHom.map_list_prod {β : Type u} {γ : Type w} [] [] (f : β →+* γ) (l : List β) :
f () = List.prod (List.map (f) l)
@[deprecated map_list_sum]
theorem RingHom.map_list_sum {β : Type u} {γ : Type w} [] [] (f : β →+* γ) (l : List β) :
f () = List.sum (List.map (f) l)
@[deprecated unop_map_list_prod]
theorem RingHom.unop_map_list_prod {β : Type u} {γ : Type w} [] [] (f : β →+* γᵐᵒᵖ) (l : List β) :
MulOpposite.unop (f ()) = 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.

@[deprecated map_multiset_prod]
theorem RingHom.map_multiset_prod {β : Type u} {γ : Type w} [] [] (f : β →+* γ) (s : ) :
f () = Multiset.prod (Multiset.map (f) s)
@[deprecated map_multiset_sum]
theorem RingHom.map_multiset_sum {β : Type u} {γ : Type w} [] [] (f : β →+* γ) (s : ) :
f () = Multiset.sum (Multiset.map (f) s)
@[deprecated map_prod]
theorem RingHom.map_prod {β : Type u} {α : Type v} {γ : Type w} [] [] (g : β →+* γ) (f : αβ) (s : ) :
g (Finset.prod s fun (x : α) => f x) = Finset.prod s fun (x : α) => g (f x)
@[deprecated map_sum]
theorem RingHom.map_sum {β : Type u} {α : Type v} {γ : Type w} [] [] (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} [] [] (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} [] [] (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} [] [] (f : αβ →+ γ) (s : ) (b : β) :
(Finset.sum s fun (x : α) => f x) b = Finset.sum s fun (x : α) => (f x) b

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

@[simp]
theorem MonoidHom.finset_prod_apply {β : Type u} {α : Type v} {γ : Type w} [] [] (f : αβ →* γ) (s : ) (b : β) :
(Finset.prod s fun (x : α) => f x) b = Finset.prod s fun (x : α) => (f x) b

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

@[simp]
theorem Finset.sum_empty {β : Type u} {α : Type v} {f : αβ} [] :
(Finset.sum fun (x : α) => f x) = 0
@[simp]
theorem Finset.prod_empty {β : Type u} {α : Type v} {f : αβ} [] :
(Finset.prod fun (x : α) => f x) = 1
theorem Finset.sum_of_empty {β : Type u} {α : Type v} {f : αβ} [] [] (s : ) :
(Finset.sum s fun (i : α) => f i) = 0
theorem Finset.prod_of_empty {β : Type u} {α : Type v} {f : αβ} [] [] (s : ) :
(Finset.prod s fun (i : α) => f i) = 1
@[simp]
theorem Finset.sum_cons {β : Type u} {α : Type v} {s : } {a : α} {f : αβ} [] (h : as) :
(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 : αβ} [] (h : as) :
(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 : αβ} [] [] :
as(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 : αβ} [] [] :
as(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 : αβ} [] [] (h : asf 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 : αβ} [] [] (h : asf 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 : αβ} [] [] (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 : αβ} [] [] (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.

theorem Finset.sum_insert_sub {α : Type v} {s : } {a : α} {M : Type u_2} [] [] (ha : as) {f : αM} :
(Finset.sum (insert a s) fun (x : α) => f x) - f a = Finset.sum s fun (x : α) => f x
theorem Finset.prod_insert_div {α : Type v} {s : } {a : α} {M : Type u_2} [] [] (ha : as) {f : αM} :
(Finset.prod (insert a s) fun (x : α) => f x) / f a = Finset.prod s fun (x : α) => f x
@[simp]
theorem Finset.sum_singleton {β : Type u} {α : Type v} [] (f : αβ) (a : α) :
(Finset.sum {a} fun (x : α) => f x) = f a
@[simp]
theorem Finset.prod_singleton {β : Type u} {α : Type v} [] (f : αβ) (a : α) :
(Finset.prod {a} fun (x : α) => f x) = f a
theorem Finset.sum_pair {β : Type u} {α : Type v} {f : αβ} [] [] {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 : αβ} [] [] {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.sum s fun (_x : α) => 0) = 0
@[simp]
theorem Finset.prod_const_one {β : Type u} {α : Type v} {s : } [] :
(Finset.prod s fun (_x : α) => 1) = 1
@[simp]
theorem Finset.sum_image {β : Type u} {α : Type v} {γ : Type w} {f : αβ} [] [] {s : } {g : γα} :
(xs, ys, g 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 : αβ} [] [] {s : } {g : γα} :
(xs, ys, g 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} [] (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} [] (s : ) (e : α γ) (f : γβ) :
(Finset.prod () fun (x : γ) => f x) = Finset.prod s fun (x : α) => f (e x)
theorem Finset.sum_attach {β : Type u} {α : Type v} [] (s : ) (f : αβ) :
(Finset.sum () fun (x : { x : α // x s }) => f x) = Finset.sum s fun (x : α) => f x
theorem Finset.prod_attach {β : Type u} {α : Type v} [] (s : ) (f : αβ) :
(Finset.prod () fun (x : { x : α // x s }) => f x) = Finset.prod s fun (x : α) => f x
theorem Finset.sum_congr {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} {g : αβ} [] (h : s₁ = s₂) :
(xs₂, f x = g x)Finset.sum s₁ f = Finset.sum s₂ g
theorem Finset.prod_congr {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} {g : αβ} [] (h : s₁ = s₂) :
(xs₂, f x = g x)Finset.prod s₁ f = Finset.prod s₂ g
theorem Finset.sum_eq_zero {β : Type u} {α : Type v} [] {f : αβ} {s : } (h : xs, f x = 0) :
(Finset.sum s fun (x : α) => f x) = 0
theorem Finset.prod_eq_one {β : Type u} {α : Type v} [] {f : αβ} {s : } (h : xs, f x = 1) :
(Finset.prod s fun (x : α) => f x) = 1
theorem Finset.sum_disjUnion {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [] (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 : αβ} [] (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_disjiUnion {ι : Type u_1} {β : Type u} {α : Type v} {f : αβ} [] (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_disjiUnion {ι : Type u_1} {β : Type u} {α : Type v} {f : αβ} [] (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 : αβ} [] [] :
((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 : αβ} [] [] :
((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 : αβ} [] [] (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 : αβ} [] [] (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} [] (s : ) (p : αProp) [] [(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} [] (s : ) (p : αProp) [] [(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} [] (s : ) (f : αβ) :
@[simp]
theorem Finset.prod_to_list {β : Type u} {α : Type v} [] (s : ) (f : αβ) :
theorem Equiv.Perm.sum_comp {β : Type u} {α : Type v} [] (σ : ) (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} [] (σ : ) (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} [] (σ : ) (s : ) (f : ααβ) (hs : {a : α | σ a a} s) :
(Finset.sum s fun (x : α) => f (σ x) x) = Finset.sum s fun (x : α) => f x (σ.symm x)
theorem Equiv.Perm.prod_comp' {β : Type u} {α : Type v} [] (σ : ) (s : ) (f : ααβ) (hs : {a : α | σ a a} s) :
(Finset.prod s fun (x : α) => f (σ x) x) = Finset.prod s fun (x : α) => f x (σ.symm x)
theorem Finset.sum_powerset_insert {β : Type u} {α : Type v} {s : } {a : α} [] [] (ha : as) (f : β) :
(Finset.sum (Finset.powerset (insert a s)) fun (t : ) => f t) = (Finset.sum () fun (t : ) => f t) + Finset.sum () fun (t : ) => f (insert a t)

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

theorem Finset.prod_powerset_insert {β : Type u} {α : Type v} {s : } {a : α} [] [] (ha : as) (f : β) :
(Finset.prod (Finset.powerset (insert a s)) fun (t : ) => f t) = (Finset.prod () fun (t : ) => f t) * Finset.prod () fun (t : ) => f (insert a t)

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

theorem Finset.sum_powerset_cons {β : Type u} {α : Type v} {s : } {a : α} [] (ha : as) (f : β) :
(Finset.sum (Finset.powerset (Finset.cons a s ha)) fun (t : ) => f t) = (Finset.sum () fun (t : ) => f t) + Finset.sum () fun (t : { x : // }) => f (Finset.cons a t (_ : at))

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

theorem Finset.prod_powerset_cons {β : Type u} {α : Type v} {s : } {a : α} [] (ha : as) (f : β) :
(Finset.prod (Finset.powerset (Finset.cons a s ha)) fun (t : ) => f t) = (Finset.prod () fun (t : ) => f t) * Finset.prod () fun (t : { x : // }) => f (Finset.cons a t (_ : at))

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

theorem Finset.sum_powerset {β : Type u} {α : Type v} [] (s : ) (f : β) :
(Finset.sum () fun (t : ) => f t) = Finset.sum (Finset.range (s.card + 1)) fun (j : ) => Finset.sum () fun (t : ) => f t

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

theorem Finset.prod_powerset {β : Type u} {α : Type v} [] (s : ) (f : β) :
(Finset.prod () fun (t : ) => f t) = Finset.prod (Finset.range (s.card + 1)) fun (j : ) => Finset.prod () fun (t : ) => f t

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

theorem IsCompl.sum_add_sum {β : Type u} {α : Type v} [] [] {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} [] [] {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} [] [] [] (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} [] [] [] (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} [] [] [] (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} [] [] [] (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 : αβ} [] [] (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 : αβ} [] [] (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
theorem Finset.sum_subset_zero_on_sdiff {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} {g : αβ} [] [] (h : s₁ s₂) (hg : xs₂ \ s₁, g x = 0) (hfg : xs₁, 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 : αβ} [] [] (h : s₁ s₂) (hg : xs₂ \ s₁, g x = 1) (hfg : xs₁, 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 : αβ} [] (h : s₁ s₂) (hf : xs₂, xs₁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 : αβ} [] (h : s₁ s₂) (hf : xs₂, xs₁f x = 1) :
(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} [] (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} [] (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} [] (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} [] (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_biUnion {β : Type u} {α : Type v} {γ : Type w} {f : αβ} [] [] {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_biUnion {β : Type u} {α : Type v} {γ : Type w} {f : αβ} [] [] {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} [] {σ : αType u_2} (s : ) (t : (a : α) → Finset (σ a)) (f : β) :
(Finset.sum () fun (x : (i : α) × σ i) => f x) = Finset.sum s fun (a : α) => Finset.sum (t a) fun (s : σ a) => 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} [] {σ : αType u_2} (s : ) (t : (a : α) → Finset (σ a)) (f : β) :
(Finset.prod () fun (x : (i : α) × σ i) => f x) = Finset.prod s fun (a : α) => Finset.prod (t a) fun (s : σ a) => 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} [] {σ : αType u_2} (s : ) (t : (a : α) → Finset (σ a)) (f : (a : α) → σ aβ) :
(Finset.sum s fun (a : α) => Finset.sum (t a) fun (s : σ a) => f a s) = Finset.sum () fun (x : (i : α) × σ i) => f x.fst x.snd
theorem Finset.prod_sigma' {β : Type u} {α : Type v} [] {σ : αType u_2} (s : ) (t : (a : α) → Finset (σ a)) (f : (a : α) → σ aβ) :
(Finset.prod s fun (a : α) => Finset.prod (t a) fun (s : σ a) => f a s) = Finset.prod () fun (x : (i : α) × σ i) => f x.fst x.snd
theorem Finset.sum_bij {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } {f : ια} {g : κα} (i : (a : ι) → a sκ) (hi : ∀ (a : ι) (ha : a s), i a ha t) (i_inj : ∀ (a₁ : ι) (ha₁ : a₁ s) (a₂ : ι) (ha₂ : a₂ s), i a₁ ha₁ = i a₂ ha₂a₁ = a₂) (i_surj : bt, ∃ (a : ι) (ha : a s), i a ha = b) (h : ∀ (a : ι) (ha : a s), f a = g (i a ha)) :
(Finset.sum s fun (x : ι) => f x) = Finset.sum t fun (x : κ) => g x

Reorder a sum.

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

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

theorem Finset.prod_bij {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } {f : ια} {g : κα} (i : (a : ι) → a sκ) (hi : ∀ (a : ι) (ha : a s), i a ha t) (i_inj : ∀ (a₁ : ι) (ha₁ : a₁ s) (a₂ : ι) (ha₂ : a₂ s), i a₁ ha₁ = i a₂ ha₂a₁ = a₂) (i_surj : bt, ∃ (a : ι) (ha : a s), i a ha = b) (h : ∀ (a : ι) (ha : a s), f a = g (i a ha)) :
(Finset.prod s fun (x : ι) => f x) = Finset.prod t fun (x : κ) => g x

Reorder a product.

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

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

theorem Finset.sum_bij' {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } {f : ια} {g : κα} (i : (a : ι) → a sκ) (j : (a : κ) → a tι) (hi : ∀ (a : ι) (ha : a s), i a ha t) (hj : ∀ (a : κ) (ha : a t), j a ha s) (left_inv : ∀ (a : ι) (ha : a s), j (i a ha) (_ : i a ha t) = a) (right_inv : ∀ (a : κ) (ha : a t), i (j a ha) (_ : j a ha s) = a) (h : ∀ (a : ι) (ha : a s), f a = g (i a ha)) :
(Finset.sum s fun (x : ι) => f x) = Finset.sum t fun (x : κ) => g x

Reorder a sum.

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

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

theorem Finset.prod_bij' {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } {f : ια} {g : κα} (i : (a : ι) → a sκ) (j : (a : κ) → a tι) (hi : ∀ (a : ι) (ha : a s), i a ha t) (hj : ∀ (a : κ) (ha : a t), j a ha s) (left_inv : ∀ (a : ι) (ha : a s), j (i a ha) (_ : i a ha t) = a) (right_inv : ∀ (a : κ) (ha : a t), i (j a ha) (_ : j a ha s) = a) (h : ∀ (a : ι) (ha : a s), f a = g (i a ha)) :
(Finset.prod s fun (x : ι) => f x) = Finset.prod t fun (x : κ) => g x

Reorder a product.

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

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

theorem Finset.sum_nbij {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } {f : ια} {g : κα} (i : ικ) (hi : as, i a t) (i_inj : Set.InjOn i s) (i_surj : Set.SurjOn i s t) (h : as, f a = g (i a)) :
(Finset.sum s fun (x : ι) => f x) = Finset.sum t fun (x : κ) => g x

Reorder a sum.

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

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

theorem Finset.prod_nbij {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } {f : ια} {g : κα} (i : ικ) (hi : as, i a t) (i_inj : Set.InjOn i s) (i_surj : Set.SurjOn i s t) (h : as, f a = g (i a)) :
(Finset.prod s fun (x : ι) => f x) = Finset.prod t fun (x : κ) => g x

Reorder a product.

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

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

theorem Finset.sum_nbij' {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } {f : ια} {g : κα} (i : ικ) (j : κι) (hi : as, i a t) (hj : at, j a s) (left_inv : as, j (i a) = a) (right_inv : at, i (j a) = a) (h : as, f a = g (i a)) :
(Finset.sum s fun (x : ι) => f x) = Finset.sum t fun (x : κ) => g x

Reorder a sum.

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

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

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

theorem Finset.prod_nbij' {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } {f : ια} {g : κα} (i : ικ) (j : κι) (hi : as, i a t) (hj : at, j a s) (left_inv : as, j (i a) = a) (right_inv : at, i (j a) = a) (h : as, f a = g (i a)) :
(Finset.prod s fun (x : ι) => f x) = Finset.prod t fun (x : κ) => g x

Reorder a product.

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

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

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

theorem Finset.sum_equiv {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } {f : ια} {g : κα} (e : ι κ) (hst : ∀ (i : ι), i s e i t) (hfg : is, f i = g (e i)) :
(Finset.sum s fun (i : ι) => f i) = Finset.sum t fun (i : κ) => g i

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

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

theorem Finset.prod_equiv {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } {f : ια} {g : κα} (e : ι κ) (hst : ∀ (i : ι), i s e i t) (hfg : is, f i = g (e i)) :
(Finset.prod s fun (i : ι) => f i) = Finset.prod t fun (i : κ) => g i

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

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

theorem Finset.sum_bijective {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } {f : ια} {g : κα} (e : ικ) (he : ) (hst : ∀ (i : ι), i s e i t) (hfg : is, f i = g (e i)) :
(Finset.sum s fun (i : ι) => f i) = Finset.sum t fun (i : κ) => g i

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

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

theorem Finset.prod_bijective {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } {f : ια} {g : κα} (e : ικ) (he : ) (hst : ∀ (i : ι), i s e i t) (hfg : is, f i = g (e i)) :
(Finset.prod s fun (i : ι) => f i) = Finset.prod t fun (i : κ) => g i

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

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

theorem Finset.sum_of_injOn {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } {f : ια} {g : κα} (e : ικ) (he : Set.InjOn e s) (hest : Set.MapsTo e s t) (h' : it, ie '' sg i = 0) (h : is, f i = g (e i)) :
(Finset.sum s fun (i : ι) => f i) = Finset.sum t fun (j : κ) => g j
theorem Finset.prod_of_injOn {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } {f : ια} {g : κα} (e : ικ) (he : Set.InjOn e s) (hest : Set.MapsTo e s t) (h' : it, ie '' sg i = 1) (h : is, f i = g (e i)) :
(Finset.prod s fun (i : ι) => f i) = Finset.prod t fun (j : κ) => g j
theorem Finset.sum_fiberwise_of_maps_to {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } [] {g : ικ} (h : is, g i t) (f : ια) :
(Finset.sum t fun (j : κ) => Finset.sum (Finset.filter (fun (i : ι) => g i = j) s) fun (i : ι) => f i) = Finset.sum s fun (i : ι) => f i
theorem Finset.prod_fiberwise_of_maps_to {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } [] {g : ικ} (h : is, g i t) (f : ια) :
(Finset.prod t fun (j : κ) => Finset.prod (Finset.filter (fun (i : ι) => g i = j) s) fun (i : ι) => f i) = Finset.prod s fun (i : ι) => f i
theorem Finset.sum_fiberwise_of_maps_to' {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } [] {g : ικ} (h : is, g i t) (f : κα) :
(Finset.sum t fun (j : κ) => Finset.sum (Finset.filter (fun (i : ι) => g i = j) s) fun (_i : ι) => f j) = Finset.sum s fun (i : ι) => f (g i)
theorem Finset.prod_fiberwise_of_maps_to' {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] {s : } {t : } [] {g : ικ} (h : is, g i t) (f : κα) :
(Finset.prod t fun (j : κ) => Finset.prod (Finset.filter (fun (i : ι) => g i = j) s) fun (_i : ι) => f j) = Finset.prod s fun (i : ι) => f (g i)
theorem Finset.sum_fiberwise {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] [] [] (s : ) (g : ικ) (f : ια) :
(Finset.sum Finset.univ fun (j : κ) => Finset.sum (Finset.filter (fun (i : ι) => g i = j) s) fun (i : ι) => f i) = Finset.sum s fun (i : ι) => f i
theorem Finset.prod_fiberwise {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] [] [] (s : ) (g : ικ) (f : ια) :
(Finset.prod Finset.univ fun (j : κ) => Finset.prod (Finset.filter (fun (i : ι) => g i = j) s) fun (i : ι) => f i) = Finset.prod s fun (i : ι) => f i
theorem Finset.sum_fiberwise' {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] [] [] (s : ) (g : ικ) (f : κα) :
(Finset.sum Finset.univ fun (j : κ) => Finset.sum (Finset.filter (fun (i : ι) => g i = j) s) fun (_i : ι) => f j) = Finset.sum s fun (i : ι) => f (g i)
theorem Finset.prod_fiberwise' {ι : Type u_2} {κ : Type u_3} {α : Type u_4} [] [] [] (s : ) (g : ικ) (f : κα) :
(Finset.prod Finset.univ fun (j : κ) => Finset.prod (Finset.filter (fun (i : ι) => g i = j) s) fun (_i : ι) => f j) = Finset.prod s fun (i : ι) => f (g i)
theorem Finset.sum_univ_pi {ι : Type u_1} {β : Type u} [] [] [] {κ : ιType u_2} (t : (i : ι) → Finset (κ i)) (f : ((i : ι) → i Finset.univκ i)β) :
(Finset.sum (Finset.pi Finset.univ t) fun (x : (a : ι) → a Finset.univκ a) => f x) = Finset.sum () fun (x : (a : ι) → κ a) => f fun (a : ι) (x_1 : a Finset.univ) => x a

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

theorem Finset.prod_univ_pi {ι : Type u_1} {β : Type u} [] [] [] {κ : ιType u_2} (t : (i : ι) → Finset (κ i)) (f : ((i : ι) → i Finset.univκ i)β) :
(Finset.prod (Finset.pi Finset.univ t) fun (x : (a : ι) → a Finset.univκ a) => f x) = Finset.prod () fun (x : (a : ι) → κ a) => f fun (a : ι) (x_1 : a Finset.univ) => x a

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

@[simp]
theorem Finset.sum_diag {β : Type u} {α : Type v} [] [] (s : ) (f : α × αβ) :
(Finset.sum () fun (i : α × α) => f i) = Finset.sum s fun (i : α) => f (i, i)
@[simp]
theorem Finset.prod_diag {β : Type u} {α : Type v} [] [] (s : ) (f : α × αβ) :
(Finset.prod () fun (i : α × α) => f i) = Finset.prod s fun (i : α) => f (i, i)
theorem Finset.sum_finset_product {β : Type u} {α : Type v} {γ : Type w} [] (r : Finset (γ × α)) (s : ) (t : γ) (h : ∀ (p : γ × α), p r p.1 s p.2 t p.1) {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} [] (r : Finset (γ × α)) (s : ) (t : γ) (h : ∀ (p : γ × α), p r p.1 s p.2 t p.1) {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} [] (r : Finset (γ × α)) (s : ) (t : γ) (h : ∀ (p : γ × α), p r p.1 s p.2 t p.1) {f : γαβ} :
(Finset.sum r fun (p : γ × α) => f p.1 p.2) = 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} [] (r : Finset (γ × α)) (s : ) (t : γ) (h : ∀ (p : γ × α), p r p.1 s p.2 t p.1) {f : γαβ} :
(Finset.prod r fun (p : γ × α) => f p.1 p.2) = 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} [] (r : Finset (α × γ)) (s : ) (t : γ) (h : ∀ (p : α × γ), p r p.2 s p.1 t p.2) {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} [] (r : Finset (α × γ)) (s : ) (t : γ) (h : ∀ (p : α × γ), p r p.2 s p.1 t p.2) {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} [] (r : Finset (α × γ)) (s : ) (t : γ) (h : ∀ (p : α × γ), p r p.2 s p.1 t p.2) {f : αγβ} :
(Finset.sum r fun (p : α × γ) => f p.1 p.2) = 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} [] (r : Finset (α × γ)) (s : ) (t : γ) (h : ∀ (p : α × γ), p r p.2 s p.1 t p.2) {f : αγβ} :
(Finset.prod r fun (p : α × γ) => f p.1 p.2) = Finset.prod s fun (c : γ) => Finset.prod (t c) fun (a : α) => f a c
abbrev Finset.sum_image'.match_1 {α : Type u_2} {γ : Type u_1} {s : } {g : γα} (_x : α) (motive : (∃ a ∈ s, g a = _x)Prop) :
∀ (x : ∃ a ∈ s, g a = _x), (∀ (c : γ) (hcs : c s) (hc : g c = _x), motive (_ : ∃ a ∈ s, g a = _x))motive x
Equations
• (_ : motive x) = (_ : motive x)
Instances For
theorem Finset.sum_image' {β : Type u} {α : Type v} {γ : Type w} {f : αβ} [] [] {s : } {g : γα} (h : γβ) (eq : cs, f (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 : αβ} [] [] {s : } {g : γα} (h : γβ) (eq : cs, f (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 : αβ} [] :
(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 : αβ} [] :
(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_add_sum_comm {β : Type u} {α : Type v} {s : } [] (f : αβ) (g : αβ) (h : αβ) (i : αβ) :
((Finset.sum s fun (a : α) => f a + g a) + Finset.sum s fun (a : α) => h a + i a) = (Finset.sum s fun (a : α) => f a + h a) + Finset.sum s fun (a : α) => g a + i a
theorem Finset.prod_mul_prod_comm {β : Type u} {α : Type v} {s : } [] (f : αβ) (g : αβ) (h : αβ) (i : αβ) :
((Finset.prod s fun (a : α) => f a * g a) * Finset.prod s fun (a : α) => h a * i a) = (Finset.prod s fun (a : α) => f a * h a) * Finset.prod s fun (a : α) => g a * i a
theorem Finset.sum_product {β : Type u} {α : Type v} {γ : Type w} [] {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} [] {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} [] {s : } {t : } {f : γαβ} :
(Finset.sum (s ×ˢ t) fun (x : γ × α) => f x.1 x.2) = 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} [] {s : } {t : } {f : γαβ} :
(Finset.prod (s ×ˢ t) fun (x : γ × α) => f x.1 x.2) = 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} [] {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} [] {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} [] {s : } {t : } {f : γαβ} :
(Finset.sum (s ×ˢ t) fun (x : γ × α) => f x.1 x.2) = Finset.sum t fun (y : α) => Finset.sum s fun (x : γ) => f x y

An uncurried version of Finset.sum_product_right

theorem Finset.prod_product_right' {β : Type u} {α : Type v} {γ : Type w} [] {s : } {t : } {f : γαβ} :
(Finset.prod (s ×ˢ t) fun (x : γ × α) => f x.1 x.2) = 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
• (_ : motive x) = (_ : motive x)
Instances For
theorem Finset.sum_comm' {β : Type u} {α : Type v} {γ : Type w} [] {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} [] {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} [] {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} [] {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} [] [] {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} [] [] {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_filter_of_ne {β : Type u} {α : Type v} {s : } {f : αβ} [] {p : αProp} [] (hp : xs, f 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 : αβ} [] {p : αProp} [] (hp : xs, f 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} {f : αβ} [] (s : ) [(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} {f : αβ} [] (s : ) [(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 : } [] (p : αProp) [] (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 : } [] (p : αProp) [] (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} [] {s : } {f : αβ} (a : α) (h : a s) (h₀ : bs, b af b = 0) :
(Finset.sum s fun (x : α) => f x) = f a
theorem Finset.prod_eq_single_of_mem {β : Type u} {α : Type v} [] {s : } {f : αβ} (a : α) (h : a s) (h₀ : bs, b af b = 1) :
(Finset.prod s fun (x : α) => f x) = f a
theorem Finset.sum_eq_single {β : Type u} {α : Type v} [] {s : } {f : αβ} (a : α) (h₀ : bs, b af b = 0) (h₁ : asf a = 0) :
(Finset.sum s fun (x : α) => f x) = f a
theorem Finset.prod_eq_single {β : Type u} {α : Type v} [] {s : } {f : αβ} (a : α) (h₀ : bs, b af b = 1) (h₁ : asf a = 1) :
(Finset.prod s fun (x : α) => f x) = f a
theorem Finset.sum_union_eq_left {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [] [] (hs : as₂, as₁f a = 0) :
(Finset.sum (s₁ s₂) fun (a : α) => f a) = Finset.sum s₁ fun (a : α) => f a
theorem Finset.prod_union_eq_left {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [] [] (hs : as₂, as₁f a = 1) :
(Finset.prod (s₁ s₂) fun (a : α) => f a) = Finset.prod s₁ fun (a : α) => f a
theorem Finset.sum_union_eq_right {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [] [] (hs : as₁, as₂f a = 0) :
(Finset.sum (s₁ s₂) fun (a : α) => f a) = Finset.sum s₂ fun (a : α) => f a
theorem Finset.prod_union_eq_right {β : Type u} {α : Type v} {s₁ : } {s₂ : } {f : αβ} [] [] (hs : as₁, as₂f a = 1) :
(Finset.prod (s₁ s₂) fun (a : α) => f a) = Finset.prod s₂ fun (a : α) => f a
theorem Finset.sum_eq_add_of_mem {β : Type u} {α : Type v} [] {s : } {f : αβ} (a : α) (b : α) (ha : a s) (hb : b s) (hn : a b) (h₀ : cs, c 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} [] {s : } {f : αβ} (a : α) (b : α) (ha : a s) (hb : b s) (hn : a b) (h₀ : cs, c 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} [] {s : } {f : αβ} (a : α) (b : α) (hn : a b) (h₀ : cs, c a c bf c = 0) (ha : asf a = 0) (hb : bsf b = 0) :
(Finset.sum s fun (x : α) => f x) = f a + f b
theorem Finset.prod_eq_mul {β : Type u} {α : Type v} [] {s : } {f : αβ} (a : α) (b : α) (hn : a b) (h₀ : cs, c a c bf c = 1) (ha : asf a = 1) (hb : bsf b = 1) :
(Finset.prod s fun (x : α) => f x) = f a * f b
@[simp]
theorem Finset.sum_subtype_eq_sum_filter {β : Type u} {α : Type v} {s : } [] (f : αβ) {p : αProp} [] :
(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 : } [] (f : αβ) {p : αProp} [] :
(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 : } [] (f : αβ) {p : αProp} [] (h : xs, p 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 : } [] (f : αβ) {p : αProp} [] (h : xs, p 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} [] {p : αProp} {s : Finset { x : α // p x }} {f : { x : α // p x }β} {g : αβ} (h : xs, g x = f x) :
(Finset.sum (Finset.map (Function.Embedding.subtype fun (x : α) => p x) s) fun (x : α) => g x) = Finset.sum s fun (x : { x : α // p x }) => f x

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

theorem Finset.prod_subtype_map_embedding {β : Type u} {α : Type v} [] {p : αProp} {s : Finset { x : α // p x }} {f : { x : α // p x }β} {g : αβ} (h : xs, g x = f x) :
(Finset.prod (Finset.map (Function.Embedding.subtype fun (x : α) => p x) s) fun (x : α) => g x) = Finset.prod s fun (x : { x : α // p x }) => f x

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

theorem Finset.sum_coe_sort_eq_attach {β : Type u} {α : Type v} (s : ) [] (f : { x : α // x s }β) :
(Finset.sum Finset.univ fun (i : { x : α // x s }) => f i) = Finset.sum () fun (i : { x : α // x s }) => f i
theorem Finset.prod_coe_sort_eq_attach {β : Type u} {α : Type v} (s : ) [] (f : { x : α // x s }β) :
(Finset.prod Finset.univ fun (i : { x : α // x s }) => f i) = Finset.prod () fun (i : { x : α // x s }) => f i
theorem Finset.sum_coe_sort {β : Type u} {α : Type v} (s : ) (f : αβ) [] :
(Finset.sum Finset.univ fun (i : { x : α // x s }) => f i) = Finset.sum s fun (i : α) => f i
theorem Finset.prod_coe_sort {β : Type u} {α : Type v} (s : ) (f : αβ) [] :
(Finset.prod Finset.univ fun (i : { x : α // x s }) => f i) = Finset.prod s fun (i : α) => f i
theorem Finset.sum_finset_coe {β : Type u} {α : Type v} [] (f : αβ) (s : ) :
(Finset.sum Finset.univ fun (i : s) => f i) = Finset.sum s fun (i : α) => f i
theorem Finset.prod_finset_coe {β : Type u} {α : Type v} [] (f : αβ) (s : ) :
(Finset.prod Finset.univ fun (i : s) => f i) = Finset.prod s fun (i : α) => f i
theorem Finset.sum_subtype {β : Type u} {α : Type v} [] {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} [] {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_set_coe {β : Type u} {α : Type v} {f : αβ} [] (s : Set α) [Fintype s] :
(Finset.sum Finset.univ fun (i : s) => f i) = Finset.sum () fun (i : α) => f i
theorem Finset.prod_set_coe {β : Type u} {α : Type v} {f : αβ} [] (s : Set α) [Fintype s] :
(Finset.prod Finset.univ fun (i : s) => f i) = Finset.prod () fun (i : α) => f i
abbrev Finset.sum_congr_set.match_1 {β : Type u_1} [] (s : Set β) [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
• (_ : motive x✝ x) = (_ : motive x✝ x)
Instances For
theorem Finset.sum_congr_set {α : Type u_2} [] {β : Type u_3} [] (s : Set β) [DecidablePred fun (x : β) => x s] (f : βα) (g : sα) (w : ∀ (x : β) (h : x s), f x = g { val := x, property := h }) (w' : xs, f 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.

theorem Finset.prod_congr_set {α : Type u_2} [] {β : Type u_3} [] (s : Set β) [DecidablePred fun (x : β) => x s] (f : βα) (g : sα) (w : ∀ (x : β) (h : x s), f x = g { val := x, property := h }) (w' : xs, f 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} [] {s : } {p : αProp} {hp : } [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 : { x : α // x }) => h (f x (_ : p x))) + Finset.sum (Finset.attach (Finset.filter (fun (x : α) => ¬p x) s)) fun (x : { x : α // x Finset.filter (fun (x : α) => ¬p x) s }) => h (g x (_ : ¬p x))
theorem Finset.prod_apply_dite {β : Type u} {α : Type v} {γ : Type w} [] {s : } {p : αProp} {hp : } [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 : { x : α // x }) => h (f x (_ : p x))) * Finset.prod (Finset.attach (Finset.filter (fun (x : α) => ¬p x) s)) fun (x : { x : α // x Finset.filter (fun (x : α) => ¬p x) s }) => h (g x (_ : ¬p x))
theorem Finset.sum_apply_ite {β : Type u} {α : Type v} {γ : Type w} [] {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} [] {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} [] {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 : { x : α // x }) => f x (_ : p x)) + Finset.sum (Finset.attach (Finset.filter (fun (x : α) => ¬p x) s)) fun (x : { x : α // x Finset.filter (fun (x : α) => ¬p x) s }) => g x (_ : ¬p x)
theorem Finset.prod_dite {β : Type u} {α : Type v} [] {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 : { x : α // x }) => f x (_ : p x)) * Finset.prod (Finset.attach (Finset.filter (fun (x : α) => ¬p x) s)) fun (x : { x : α // x Finset.filter (fun (x : α) => ¬p x) s }) => g x (_ : ¬p x)
theorem Finset.sum_ite {β : Type u} {α : Type v} [] {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} [] {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 : } [] {p : αProp} {hp : } (f : αβ) (g : αβ) (h : xs, ¬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 : } [] {p : αProp} {hp : } (f : αβ) (g : αβ) (h : xs, ¬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 : } [] {p : αProp} {hp : } (f : αβ) (g : αβ) (h : xs, p 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 : } [] {p : αProp} {hp : } (f : αβ) (g : αβ) (h : xs, p 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 : } [] {p : αProp} {hp : } (f : αγ) (g : αγ) (k : γβ) (h : xs, ¬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 : } [] {p : αProp} {hp : } (f : αγ) (g : αγ) (k : γβ) (h : xs, ¬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 : } [] {p : αProp} {hp : } (f : αγ) (g : αγ) (k : γβ) (h : xs, p 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 : } [] {p : αProp} {hp : } (f : αγ) (g : αγ) (k : γβ) (h : xs, p 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} [] [] (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} [] [] (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} [] [] (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} [] [] (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} [] [] (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} [] [] (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} [] [] (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} [] [] (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} [] [] (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} [] [] (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} [] [] (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} [] [] (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} [] (p : Prop) [] (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} [] (p : Prop) [] (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} [] (p : Prop) [] (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} [] (p : Prop) [] (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} [] (p : Prop) [] (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} [] (p : Prop) [] (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} {α : Type v} [] [] (a : α) (x : β) (s : ) :
(Finset.sum s fun (a' : α) => Pi.single a x a') = if a s then x else 0
@[simp]
theorem Finset.prod_pi_mulSingle' {β : Type u} {α : Type v} [] [] (a : α) (x : β) (s : ) :
(Finset.prod s fun (a' : α) => Pi.mulSingle a x a') = if a s then x else 1
@[simp]
theorem Finset.sum_pi_single {α : Type v} {β : αType u_2} [] [(a : α) → AddCommMonoid (β a)] (a : α) (f : (a : α) → β a) (s : ) :
(Finset.sum s fun (a' : α) => Pi.single a' (f a') a) = if a s then f a else 0
@[simp]
theorem Finset.prod_pi_mulSingle {α : Type v} {β : αType u_2} [] [(a : α) → CommMonoid (β a)] (a : α) (f : (a : α) → β a) (s : ) :
(Finset.prod s fun (a' : α) => Pi.mulSingle a' (f a') a) = if a s then f a else 1
theorem Finset.support_sum {ι : Type u_1} {β : Type u} {α : Type v} [] (s : ) (f : ιαβ) :
(Function.support fun (x : α) => Finset.sum s fun (i : ι) => f i x) ⋃ i ∈ s, Function.support (f i)
theorem Finset.mulSupport_prod {ι : Type u_1} {β : Type u} {α : Type v} [] (s : ) (f : ιαβ) :
(Function.mulSupport fun (x : α) => Finset.prod s fun (i : ι) => f i x) ⋃ i ∈ s, Function.mulSupport (f i)
theorem Finset.sum_indicator_subset_of_eq_zero {ι : Type u_1} {β : Type u} {α : Type v} [] [Zero α] (f : ια) (g : ιαβ) {s : } {t : } (h : s t) (hg : ∀ (a : ι), g a 0 = 0) :
(Finset.sum t fun (i : ι) => g i (Set.indicator (s) f i)) = Finset.sum s fun (i : ι) => g i (f i)

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

theorem Finset.prod_mulIndicator_subset_of_eq_one {ι : Type u_1} {β : Type u} {α : Type v} [] [One α] (f : ια) (g : ιαβ) {s : } {t : } (h : s t) (hg : ∀ (a : ι), g a 1 = 1) :
(Finset.prod t fun (i : ι) => g i (Set.mulIndicator (s) f i)) = Finset.prod s fun (i : ι) => g i (f i)

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

theorem Finset.sum_indicator_subset {ι : Type u_1} {β : Type u} [] (f : ιβ) {s : } {t : } (h : s t) :
(Finset.sum t fun (i : ι) => Set.indicator (s) f i) = Finset.sum s fun (i : ι) => f i

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

theorem Finset.prod_mulIndicator_subset {ι : Type u_1} {β : Type u} [] (f : ιβ) {s : } {t : } (h : s t) :
(Finset.prod t fun (i : ι) => Set.mulIndicator (s) f i) = Finset.prod s fun (i : ι) => f i

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

theorem Finset.sum_indicator_eq_sum_filter {ι : Type u_1} {β : Type u} [] {κ : Type u_2} (s : ) (f : ικβ) (t : ιSet κ) (g : ικ) [DecidablePred fun (i : ι) => g i t i] :
(Finset.sum s fun (i : ι) => Set.indicator (t i) (f i) (g i)) = Finset.sum (Finset.filter (fun (i : ι) => g i t i) s) fun (i : ι) => f i (g i)
theorem Finset.prod_mulIndicator_eq_prod_filter {ι : Type u_1} {β : Type u} [] {κ : Type u_2} (s : ) (f : ικβ) (t : ιSet κ) (g : ικ) [DecidablePred fun (i : ι) => g i t i] :
(Finset.prod s fun (i : ι) => Set.mulIndicator (t i) (f i) (g i)) = Finset.prod (Finset.filter (fun (i : ι) => g i t i) s) fun (i : ι) => f i (g i)
theorem Finset.sum_indicator_eq_sum_inter {ι : Type u_1} {β : Type u} [] [] (s : ) (t : ) (f : ιβ) :
(Finset.sum s fun (i : ι) => Set.indicator (t) f i) = Finset.sum (s t) fun (i : ι) => f i
theorem Finset.prod_mulIndicator_eq_prod_inter {ι : Type u_1} {β : Type u} [] [] (s : ) (t : ) (f : ιβ) :
(Finset.prod s fun (i : ι) => Set.mulIndicator (t) f i) = Finset.prod (s t) fun (i : ι) => f i
theorem Finset.indicator_sum {ι : Type u_1} {β : Type u} [] {κ : Type u_2} (s : ) (t : Set κ) (f : ικβ) :
Set.indicator t (Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => Set.indicator t (f i)
theorem Finset.mulIndicator_prod {ι : Type u_1} {β : Type u} [] {κ : Type u_2} (s : ) (t : Set κ) (f : ικβ) :
Set.mulIndicator t (Finset.prod s fun (i : ι) => f i) = Finset.prod s fun (i : ι) => Set.mulIndicator t (f i)
theorem Finset.indicator_biUnion {ι : Type u_1} {β : Type u} [] {κ : Type u_3} (s : ) (t : ιSet κ) {f : κβ} :
Set.PairwiseDisjoint (s) tSet.indicator (⋃ i ∈ s, t i) f = fun (a : κ) => Finset.sum s fun (i : ι) => Set.indicator (t i) f a
theorem Finset.mulIndicator_biUnion {ι : Type u_1} {β : Type u} [] {κ : Type u_3} (s : ) (t : ιSet κ) {f : κβ} :
Set.PairwiseDisjoint (s) tSet.mulIndicator (⋃ i ∈ s, t i) f = fun (a : κ) => Finset.prod s fun (i : ι) => Set.mulIndicator (t i) f a
theorem Finset.indicator_biUnion_apply {ι : Type u_1} {β : Type u} [] {κ : Type u_3} (s : ) (t : ιSet κ) {f : κβ} (h : Set.PairwiseDisjoint (s) t) (x : κ) :
Set.indicator (⋃ i ∈ s, t i) f x = Finset.sum s fun (i : ι) => Set.indicator (t i) f x
theorem Finset.mulIndicator_biUnion_apply {ι : Type u_1} {β : Type u} [] {κ : Type u_3} (s : ) (t : ιSet κ) {f : κβ} (h : Set.PairwiseDisjoint (s) t) (x : κ) :
Set.mulIndicator (⋃ i ∈ s, t i) f x = Finset.prod s fun (i : ι) => Set.mulIndicator (t i) f x
theorem Finset.sum_bij_ne_zero {β : Type u} {α : Type v} {γ : Type w} [] {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₁ : α) (h₁₁ : a₁ s) (h₁₂ : f a₁ 0) (a₂ : α) (h₂₁ : a₂ s) (h₂₂ : f a₂ 0), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂a₁ = a₂) (i_surj : bt, g b 0∃ (a : α) (h₁ : a s) (h₂ : f a 0), i a h₁ h₂ = b) (h : ∀ (a : α) (h₁ : a s) (h₂ : f a 0), f a = g (i a h₁ h₂)) :
(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} [] {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₁ : α) (h₁₁ : a₁ s) (h₁₂ : f a₁ 1) (a₂ : α) (h₂₁ : a₂ s) (h₂₂ : f a₂ 1), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂a₁ = a₂) (i_surj : bt, g b 1∃ (a : α) (h₁ : a s) (h₂ : f a 1), i a h₁ h₂ = b) (h : ∀ (a : α) (h₁ : a s) (h₂ : f a 1), f a = g (i a h₁ h₂)) :
(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 : } [] {p : αProp} {hp : } (h : xs, ¬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 : { x : α // x s }) => g x (_ : ¬p x)
theorem Finset.prod_dite_of_false {β : Type u} {α : Type v} {s : } [] {p : αProp} {hp : } (h : xs, ¬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 : { x : α // x s }) => g x (_ : ¬p x)
theorem Finset.sum_dite_of_true {β : Type u} {α : Type v} {s : } [] {p : αProp} {hp : } (h : xs, 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 : { x : α // x s }) => f x (_ : p x)
theorem Finset.prod_dite_of_true {β : Type u} {α : Type v} {s : } [] {p : αProp} {hp : } (h : xs, 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 : { x : α // x s }) => f x (_ : p x)
theorem Finset.nonempty_of_sum_ne_zero {β : Type u} {α : Type v} {s : } {f : αβ} [] (h : (Finset.sum s fun (x : α) => f x) 0) :
s.Nonempty
theorem Finset.nonempty_of_prod_ne_one {β : Type u} {α : Type v} {s : } {f : αβ} [] (h : (Finset.prod s fun (x : α) => f x) 1) :
s.Nonempty
theorem Finset.exists_ne_zero_of_sum_ne_zero {β : Type u} {α : Type v} {s : } {f : αβ} [] (h : (Finset.sum s fun (x : α) => f x) 0) :
∃ a ∈ s, f a 0
theorem Finset.exists_ne_one_of_prod_ne_one {β : Type u} {α : Type v} {s : } {f : αβ} [] (h : (Finset.prod s fun (x : α) => f x) 1) :
∃ a ∈ s, f a 1
theorem Finset.sum_range_succ_comm {β : Type u} [] (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} [] (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} [] (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} [] (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
• (_ : motive x) = (_ : motive x)
Instances For
theorem Finset.sum_range_succ' {β : Type u} [] (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} [] (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} [] {u : β} {N : } (hu : nN, u n = 0) {n : } (hn : N n) :
(Finset.sum () fun (k : ) => u k) = Finset.sum () fun (k : ) => u k
theorem Finset.eventually_constant_prod {β : Type u} [] {u : β} {N : } (hu : nN, u n = 1) {n : } (hn : N n) :
(Finset.prod () fun (k : ) => u k) = Finset.prod () fun (k : ) => u k
theorem Finset.sum_range_add {β : Type u} [] (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} [] (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_2} [] (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_2} [] (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} [] (f : β) :
(Finset.sum () fun (k : ) => f k) = 0
theorem Finset.prod_range_zero {β : Type u} [] (f : β) :
(Finset.prod () fun (k : ) => f k) = 1
theorem Finset.sum_range_one {β : Type u} [] (f : β) :
(Finset.sum () fun (k : ) => f k) = f 0
theorem Finset.prod_range_one {β : Type u} [] (f : β) :
(Finset.prod () fun (k : ) => f k) = f 0
theorem Finset.sum_list_map_count {α : Type v} [] (l : List α) {M : Type u_2} [] (f : αM) :
List.sum (List.map f l) = Finset.sum () fun (m : α) => f m
theorem Finset.prod_list_map_count {α : Type v} [] (l : List α) {M : Type u_2} [] (f : αM) :
List.prod (List.map f l) = Finset.prod () fun (m : α) => f m ^
theorem Finset.sum_list_count {α : Type v} [] [] (s : List α) :
= Finset.sum () fun (m : α) => m
theorem Finset.prod_list_count {α : Type v} [] [] (s : List α) :
= Finset.prod () fun (m : α) => m ^
theorem Finset.sum_list_count_of_subset {α : Type v} [] [] (m : List α) (s : ) (hs : ) :
= Finset.sum s fun (i : α) => i
theorem Finset.prod_list_count_of_subset {α : Type v} [] [] (m : List α) (s : ) (hs : ) :
= Finset.prod s fun (i : α) => i ^
theorem Finset.sum_filter_count_eq_countP {α : Type v} [] (p : αProp) [] (l : List α) :
(Finset.sum () fun (x : α) => ) = List.countP (fun (b : α) => decide (p b)) l
theorem Finset.sum_multiset_map_count {α : Type v} [] (s : ) {M : Type u_2} [] (f : αM) :
Multiset.sum () = Finset.sum fun (m : α) => f m
theorem Finset.prod_multiset_map_count {α : Type v} [] (s : ) {M : Type u_2} [] (f : αM) :
= Finset.prod fun (m : α) => f m ^
theorem Finset.sum_multiset_count {α : Type v} [] [] (s : ) :
= Finset.sum fun (m : α) => m
theorem Finset.prod_multiset_count {α : Type v} [] [] (s : ) :
= Finset.prod fun (m : α) => m ^
theorem Finset.sum_multiset_count_of_subset {α : Type v} [] [] (m : ) (s : ) (hs : ) :
= Finset.sum s fun (i : α) => i
theorem Finset.prod_multiset_count_of_subset {α : Type v} [] [] (m : ) (s :