mathlib3 documentation

algebra.big_operators.basic

Big operators #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Notation #

We introduce the following notation, localized in big_operators. To enable the notation, use open_locale big_operators.

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.

@[protected]
def finset.sum {β : Type u} {α : Type v} [add_comm_monoid β] (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
@[protected]
def finset.prod {β : Type u} {α : Type v} [comm_monoid β] (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.prod_mk {β : Type u} {α : Type v} [comm_monoid β] (s : multiset α) (hs : s.nodup) (f : α β) :
{val := s, nodup := hs}.prod f = (multiset.map f s).prod
@[simp]
theorem finset.sum_mk {β : Type u} {α : Type v} [add_comm_monoid β] (s : multiset α) (hs : s.nodup) (f : α β) :
{val := s, nodup := hs}.sum f = (multiset.map f s).sum
@[simp]
theorem finset.sum_val {α : Type v} [add_comm_monoid α] (s : finset α) :
s.val.sum = s.sum id
@[simp]
theorem finset.prod_val {α : Type v} [comm_monoid α] (s : finset α) :

There is no established mathematical convention for the operator precedence of big operators like and . We will have to make a choice.

Online discussions, such as https://math.stackexchange.com/q/185538/30839 seem to suggest that and should have the same precedence, and that this should be somewhere between * and +. The latter have precedence levels 70 and 65 respectively, and we therefore choose the level 67.

In practice, this means that parentheses should be placed as follows:

 k in K, (a k + b k) =  k in K, a k +  k in K, b k 
   k in K, a k * b k = ( k in K, a k) * ( k in K, b k)

(Example taken from page 490 of Knuth's Concrete Mathematics.)

theorem finset.prod_eq_multiset_prod {β : Type u} {α : Type v} [comm_monoid β] (s : finset α) (f : α β) :
s.prod (λ (x : α), f x) = (multiset.map f s.val).prod
theorem finset.sum_eq_multiset_sum {β : Type u} {α : Type v} [add_comm_monoid β] (s : finset α) (f : α β) :
s.sum (λ (x : α), f x) = (multiset.map f s.val).sum
theorem finset.prod_eq_fold {β : Type u} {α : Type v} [comm_monoid β] (s : finset α) (f : α β) :
s.prod (λ (x : α), f x) = finset.fold has_mul.mul 1 f s
theorem finset.sum_eq_fold {β : Type u} {α : Type v} [add_comm_monoid β] (s : finset α) (f : α β) :
s.sum (λ (x : α), f x) = finset.fold has_add.add 0 f s
@[simp]
theorem finset.sum_multiset_singleton {α : Type v} (s : finset α) :
s.sum (λ (x : α), {x}) = s.val
theorem map_sum {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] [add_comm_monoid γ] {G : Type u_1} [add_monoid_hom_class G β γ] (g : G) (f : α β) (s : finset α) :
g (s.sum (λ (x : α), f x)) = s.sum (λ (x : α), g (f x))
theorem map_prod {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] [comm_monoid γ] {G : Type u_1} [monoid_hom_class G β γ] (g : G) (f : α β) (s : finset α) :
g (s.prod (λ (x : α), f x)) = s.prod (λ (x : α), g (f x))
@[protected]
theorem add_monoid_hom.map_sum {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] [add_comm_monoid γ] (g : β →+ γ) (f : α β) (s : finset α) :
g (s.sum (λ (x : α), f x)) = s.sum (λ (x : α), g (f x))

Deprecated: use _root_.map_sum instead.

@[protected]
theorem monoid_hom.map_prod {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] [comm_monoid γ] (g : β →* γ) (f : α β) (s : finset α) :
g (s.prod (λ (x : α), f x)) = s.prod (λ (x : α), g (f x))

Deprecated: use _root_.map_prod instead.

@[protected]
theorem add_equiv.map_sum {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] [add_comm_monoid γ] (g : β ≃+ γ) (f : α β) (s : finset α) :
g (s.sum (λ (x : α), f x)) = s.sum (λ (x : α), g (f x))

Deprecated: use _root_.map_sum instead.

@[protected]
theorem mul_equiv.map_prod {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] [comm_monoid γ] (g : β ≃* γ) (f : α β) (s : finset α) :
g (s.prod (λ (x : α), f x)) = s.prod (λ (x : α), g (f x))

Deprecated: use _root_.map_prod instead.

@[protected]
theorem ring_hom.map_list_prod {β : Type u} {γ : Type w} [semiring β] [semiring γ] (f : β →+* γ) (l : list β) :

Deprecated: use _root_.map_list_prod instead.

@[protected]
theorem ring_hom.map_list_sum {β : Type u} {γ : Type w} [non_assoc_semiring β] [non_assoc_semiring γ] (f : β →+* γ) (l : list β) :

Deprecated: use _root_.map_list_sum instead.

@[protected]

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

Deprecated: use _root_.unop_map_list_prod instead.

@[protected]
theorem ring_hom.map_multiset_prod {β : Type u} {γ : Type w} [comm_semiring β] [comm_semiring γ] (f : β →+* γ) (s : multiset β) :

Deprecated: use _root_.map_multiset_prod instead.

@[protected]
theorem ring_hom.map_multiset_sum {β : Type u} {γ : Type w} [non_assoc_semiring β] [non_assoc_semiring γ] (f : β →+* γ) (s : multiset β) :

Deprecated: use _root_.map_multiset_sum instead.

@[protected]
theorem ring_hom.map_prod {β : Type u} {α : Type v} {γ : Type w} [comm_semiring β] [comm_semiring γ] (g : β →+* γ) (f : α β) (s : finset α) :
g (s.prod (λ (x : α), f x)) = s.prod (λ (x : α), g (f x))

Deprecated: use _root_.map_prod instead.

@[protected]
theorem ring_hom.map_sum {β : Type u} {α : Type v} {γ : Type w} [non_assoc_semiring β] [non_assoc_semiring γ] (g : β →+* γ) (f : α β) (s : finset α) :
g (s.sum (λ (x : α), f x)) = s.sum (λ (x : α), g (f x))

Deprecated: use _root_.map_sum instead.

theorem add_monoid_hom.coe_finset_sum {β : Type u} {α : Type v} {γ : Type w} [add_zero_class β] [add_comm_monoid γ] (f : α β →+ γ) (s : finset α) :
(s.sum (λ (x : α), f x)) = s.sum (λ (x : α), (f x))
theorem monoid_hom.coe_finset_prod {β : Type u} {α : Type v} {γ : Type w} [mul_one_class β] [comm_monoid γ] (f : α β →* γ) (s : finset α) :
(s.prod (λ (x : α), f x)) = s.prod (λ (x : α), (f x))
@[simp]
theorem add_monoid_hom.finset_sum_apply {β : Type u} {α : Type v} {γ : Type w} [add_zero_class β] [add_comm_monoid γ] (f : α β →+ γ) (s : finset α) (b : β) :
(s.sum (λ (x : α), f x)) b = s.sum (λ (x : α), (f x) b)
@[simp]
theorem monoid_hom.finset_prod_apply {β : Type u} {α : Type v} {γ : Type w} [mul_one_class β] [comm_monoid γ] (f : α β →* γ) (s : finset α) (b : β) :
(s.prod (λ (x : α), f x)) b = s.prod (λ (x : α), (f x) b)
@[simp]
theorem finset.sum_empty {β : Type u} {α : Type v} {f : α β} [add_comm_monoid β] :
.sum (λ (x : α), f x) = 0
@[simp]
theorem finset.prod_empty {β : Type u} {α : Type v} {f : α β} [comm_monoid β] :
.prod (λ (x : α), f x) = 1
theorem finset.prod_of_empty {β : Type u} {α : Type v} {f : α β} [comm_monoid β] [is_empty α] (s : finset α) :
s.prod (λ (i : α), f i) = 1
theorem finset.sum_of_empty {β : Type u} {α : Type v} {f : α β} [add_comm_monoid β] [is_empty α] (s : finset α) :
s.sum (λ (i : α), f i) = 0
@[simp]
theorem finset.sum_cons {β : Type u} {α : Type v} {s : finset α} {a : α} {f : α β} [add_comm_monoid β] (h : a s) :
(finset.cons a s h).sum (λ (x : α), f x) = f a + s.sum (λ (x : α), f x)
@[simp]
theorem finset.prod_cons {β : Type u} {α : Type v} {s : finset α} {a : α} {f : α β} [comm_monoid β] (h : a s) :
(finset.cons a s h).prod (λ (x : α), f x) = f a * s.prod (λ (x : α), f x)
@[simp]
theorem finset.prod_insert {β : Type u} {α : Type v} {s : finset α} {a : α} {f : α β} [comm_monoid β] [decidable_eq α] :
a s (has_insert.insert a s).prod (λ (x : α), f x) = f a * s.prod (λ (x : α), f x)
@[simp]
theorem finset.sum_insert {β : Type u} {α : Type v} {s : finset α} {a : α} {f : α β} [add_comm_monoid β] [decidable_eq α] :
a s (has_insert.insert a s).sum (λ (x : α), f x) = f a + s.sum (λ (x : α), f x)
@[simp]
theorem finset.sum_insert_of_eq_zero_if_not_mem {β : Type u} {α : Type v} {s : finset α} {a : α} {f : α β} [add_comm_monoid β] [decidable_eq α] (h : a s f a = 0) :
(has_insert.insert a s).sum (λ (x : α), f x) = s.sum (λ (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 : α β} [comm_monoid β] [decidable_eq α] (h : a s f a = 1) :
(has_insert.insert a s).prod (λ (x : α), f x) = s.prod (λ (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 : α β} [add_comm_monoid β] [decidable_eq α] (h : f a = 0) :
(has_insert.insert a s).sum (λ (x : α), f x) = s.sum (λ (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 : α β} [comm_monoid β] [decidable_eq α] (h : f a = 1) :
(has_insert.insert a s).prod (λ (x : α), f x) = s.prod (λ (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.prod_singleton {β : Type u} {α : Type v} {a : α} {f : α β} [comm_monoid β] :
{a}.prod (λ (x : α), f x) = f a
@[simp]
theorem finset.sum_singleton {β : Type u} {α : Type v} {a : α} {f : α β} [add_comm_monoid β] :
{a}.sum (λ (x : α), f x) = f a
theorem finset.prod_pair {β : Type u} {α : Type v} {f : α β} [comm_monoid β] [decidable_eq α] {a b : α} (h : a b) :
{a, b}.prod (λ (x : α), f x) = f a * f b
theorem finset.sum_pair {β : Type u} {α : Type v} {f : α β} [add_comm_monoid β] [decidable_eq α] {a b : α} (h : a b) :
{a, b}.sum (λ (x : α), f x) = f a + f b
@[simp]
theorem finset.prod_const_one {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] :
s.prod (λ (x : α), 1) = 1
@[simp]
theorem finset.sum_const_zero {β : Type u} {α : Type v} {s : finset α} [add_comm_monoid β] :
s.sum (λ (x : α), 0) = 0
@[simp]
theorem finset.sum_image {β : Type u} {α : Type v} {γ : Type w} {f : α β} [add_comm_monoid β] [decidable_eq α] {s : finset γ} {g : γ α} :
( (x : γ), x s (y : γ), y s g x = g y x = y) (finset.image g s).sum (λ (x : α), f x) = s.sum (λ (x : γ), f (g x))
@[simp]
theorem finset.prod_image {β : Type u} {α : Type v} {γ : Type w} {f : α β} [comm_monoid β] [decidable_eq α] {s : finset γ} {g : γ α} :
( (x : γ), x s (y : γ), y s g x = g y x = y) (finset.image g s).prod (λ (x : α), f x) = s.prod (λ (x : γ), f (g x))
@[simp]
theorem finset.sum_map {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] (s : finset α) (e : α γ) (f : γ β) :
(finset.map e s).sum (λ (x : γ), f x) = s.sum (λ (x : α), f (e x))
@[simp]
theorem finset.prod_map {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] (s : finset α) (e : α γ) (f : γ β) :
(finset.map e s).prod (λ (x : γ), f x) = s.prod (λ (x : α), f (e x))
theorem finset.prod_congr {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f g : α β} [comm_monoid β] (h : s₁ = s₂) :
( (x : α), x s₂ f x = g x) s₁.prod f = s₂.prod g
theorem finset.sum_congr {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f g : α β} [add_comm_monoid β] (h : s₁ = s₂) :
( (x : α), x s₂ f x = g x) s₁.sum f = s₂.sum g
theorem finset.sum_disj_union {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α β} [add_comm_monoid β] (h : disjoint s₁ s₂) :
(s₁.disj_union s₂ h).sum (λ (x : α), f x) = s₁.sum (λ (x : α), f x) + s₂.sum (λ (x : α), f x)
theorem finset.prod_disj_union {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α β} [comm_monoid β] (h : disjoint s₁ s₂) :
(s₁.disj_union s₂ h).prod (λ (x : α), f x) = s₁.prod (λ (x : α), f x) * s₂.prod (λ (x : α), f x)
theorem finset.prod_disj_Union {ι : Type u_1} {β : Type u} {α : Type v} {f : α β} [comm_monoid β] (s : finset ι) (t : ι finset α) (h : s.pairwise_disjoint t) :
(s.disj_Union t h).prod (λ (x : α), f x) = s.prod (λ (i : ι), (t i).prod (λ (x : α), f x))
theorem finset.sum_disj_Union {ι : Type u_1} {β : Type u} {α : Type v} {f : α β} [add_comm_monoid β] (s : finset ι) (t : ι finset α) (h : s.pairwise_disjoint t) :
(s.disj_Union t h).sum (λ (x : α), f x) = s.sum (λ (i : ι), (t i).sum (λ (x : α), f x))
theorem finset.sum_union_inter {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α β} [add_comm_monoid β] [decidable_eq α] :
(s₁ s₂).sum (λ (x : α), f x) + (s₁ s₂).sum (λ (x : α), f x) = s₁.sum (λ (x : α), f x) + s₂.sum (λ (x : α), f x)
theorem finset.prod_union_inter {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α β} [comm_monoid β] [decidable_eq α] :
(s₁ s₂).prod (λ (x : α), f x) * (s₁ s₂).prod (λ (x : α), f x) = s₁.prod (λ (x : α), f x) * s₂.prod (λ (x : α), f x)
theorem finset.prod_union {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α β} [comm_monoid β] [decidable_eq α] (h : disjoint s₁ s₂) :
(s₁ s₂).prod (λ (x : α), f x) = s₁.prod (λ (x : α), f x) * s₂.prod (λ (x : α), f x)
theorem finset.sum_union {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α β} [add_comm_monoid β] [decidable_eq α] (h : disjoint s₁ s₂) :
(s₁ s₂).sum (λ (x : α), f x) = s₁.sum (λ (x : α), f x) + s₂.sum (λ (x : α), f x)
theorem finset.sum_filter_add_sum_filter_not {β : Type u} {α : Type v} [add_comm_monoid β] (s : finset α) (p : α Prop) [decidable_pred p] [decidable_pred (λ (x : α), ¬p x)] (f : α β) :
(finset.filter p s).sum (λ (x : α), f x) + (finset.filter (λ (x : α), ¬p x) s).sum (λ (x : α), f x) = s.sum (λ (x : α), f x)
theorem finset.prod_filter_mul_prod_filter_not {β : Type u} {α : Type v} [comm_monoid β] (s : finset α) (p : α Prop) [decidable_pred p] [decidable_pred (λ (x : α), ¬p x)] (f : α β) :
(finset.filter p s).prod (λ (x : α), f x) * (finset.filter (λ (x : α), ¬p x) s).prod (λ (x : α), f x) = s.prod (λ (x : α), f x)
@[simp]
theorem finset.prod_to_list {β : Type u} {α : Type v} [comm_monoid β] (s : finset α) (f : α β) :
@[simp]
theorem finset.sum_to_list {β : Type u} {α : Type v} [add_comm_monoid β] (s : finset α) (f : α β) :
theorem equiv.perm.sum_comp {β : Type u} {α : Type v} [add_comm_monoid β] (σ : equiv.perm α) (s : finset α) (f : α β) (hs : {a : α | σ a a} s) :
s.sum (λ (x : α), f (σ x)) = s.sum (λ (x : α), f x)
theorem equiv.perm.prod_comp {β : Type u} {α : Type v} [comm_monoid β] (σ : equiv.perm α) (s : finset α) (f : α β) (hs : {a : α | σ a a} s) :
s.prod (λ (x : α), f (σ x)) = s.prod (λ (x : α), f x)
theorem equiv.perm.sum_comp' {β : Type u} {α : Type v} [add_comm_monoid β] (σ : equiv.perm α) (s : finset α) (f : α α β) (hs : {a : α | σ a a} s) :
s.sum (λ (x : α), f (σ x) x) = s.sum (λ (x : α), f x ((equiv.symm σ) x))
theorem equiv.perm.prod_comp' {β : Type u} {α : Type v} [comm_monoid β] (σ : equiv.perm α) (s : finset α) (f : α α β) (hs : {a : α | σ a a} s) :
s.prod (λ (x : α), f (σ x) x) = s.prod (λ (x : α), f x ((equiv.symm σ) x))
theorem is_compl.sum_add_sum {β : Type u} {α : Type v} [fintype α] [add_comm_monoid β] {s t : finset α} (h : is_compl s t) (f : α β) :
s.sum (λ (i : α), f i) + t.sum (λ (i : α), f i) = finset.univ.sum (λ (i : α), f i)
theorem is_compl.prod_mul_prod {β : Type u} {α : Type v} [fintype α] [comm_monoid β] {s t : finset α} (h : is_compl s t) (f : α β) :
s.prod (λ (i : α), f i) * t.prod (λ (i : α), f i) = finset.univ.prod (λ (i : α), f i)
theorem finset.sum_add_sum_compl {β : Type u} {α : Type v} [add_comm_monoid β] [fintype α] [decidable_eq α] (s : finset α) (f : α β) :
s.sum (λ (i : α), f i) + s.sum (λ (i : α), f i) = finset.univ.sum (λ (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} [comm_monoid β] [fintype α] [decidable_eq α] (s : finset α) (f : α β) :
s.prod (λ (i : α), f i) * s.prod (λ (i : α), f i) = finset.univ.prod (λ (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.prod_compl_mul_prod {β : Type u} {α : Type v} [comm_monoid β] [fintype α] [decidable_eq α] (s : finset α) (f : α β) :
s.prod (λ (i : α), f i) * s.prod (λ (i : α), f i) = finset.univ.prod (λ (i : α), f i)
theorem finset.sum_compl_add_sum {β : Type u} {α : Type v} [add_comm_monoid β] [fintype α] [decidable_eq α] (s : finset α) (f : α β) :
s.sum (λ (i : α), f i) + s.sum (λ (i : α), f i) = finset.univ.sum (λ (i : α), f i)
theorem finset.prod_sdiff {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α β} [comm_monoid β] [decidable_eq α] (h : s₁ s₂) :
(s₂ \ s₁).prod (λ (x : α), f x) * s₁.prod (λ (x : α), f x) = s₂.prod (λ (x : α), f x)
theorem finset.sum_sdiff {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α β} [add_comm_monoid β] [decidable_eq α] (h : s₁ s₂) :
(s₂ \ s₁).sum (λ (x : α), f x) + s₁.sum (λ (x : α), f x) = s₂.sum (λ (x : α), f x)
@[simp]
theorem finset.sum_disj_sum {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] (s : finset α) (t : finset γ) (f : α γ β) :
(s.disj_sum t).sum (λ (x : α γ), f x) = s.sum (λ (x : α), f (sum.inl x)) + t.sum (λ (x : γ), f (sum.inr x))
@[simp]
theorem finset.prod_disj_sum {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] (s : finset α) (t : finset γ) (f : α γ β) :
(s.disj_sum t).prod (λ (x : α γ), f x) = s.prod (λ (x : α), f (sum.inl x)) * t.prod (λ (x : γ), f (sum.inr x))
theorem finset.sum_sum_elim {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] (s : finset α) (t : finset γ) (f : α β) (g : γ β) :
(s.disj_sum t).sum (λ (x : α γ), sum.elim f g x) = s.sum (λ (x : α), f x) + t.sum (λ (x : γ), g x)
theorem finset.prod_sum_elim {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] (s : finset α) (t : finset γ) (f : α β) (g : γ β) :
(s.disj_sum t).prod (λ (x : α γ), sum.elim f g x) = s.prod (λ (x : α), f x) * t.prod (λ (x : γ), g x)
theorem finset.prod_bUnion {β : Type u} {α : Type v} {γ : Type w} {f : α β} [comm_monoid β] [decidable_eq α] {s : finset γ} {t : γ finset α} (hs : s.pairwise_disjoint t) :
(s.bUnion t).prod (λ (x : α), f x) = s.prod (λ (x : γ), (t x).prod (λ (i : α), f i))
theorem finset.sum_bUnion {β : Type u} {α : Type v} {γ : Type w} {f : α β} [add_comm_monoid β] [decidable_eq α] {s : finset γ} {t : γ finset α} (hs : s.pairwise_disjoint t) :
(s.bUnion t).sum (λ (x : α), f x) = s.sum (λ (x : γ), (t x).sum (λ (i : α), f i))
theorem finset.prod_sigma {β : Type u} {α : Type v} [comm_monoid β] {σ : α Type u_1} (s : finset α) (t : Π (a : α), finset (σ a)) (f : sigma σ β) :
(s.sigma t).prod (λ (x : Σ (i : α), σ i), f x) = s.prod (λ (a : α), (t a).prod (λ (s : σ a), f a, s⟩))

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

theorem finset.sum_sigma {β : Type u} {α : Type v} [add_comm_monoid β] {σ : α Type u_1} (s : finset α) (t : Π (a : α), finset (σ a)) (f : sigma σ β) :
(s.sigma t).sum (λ (x : Σ (i : α), σ i), f x) = s.sum (λ (a : α), (t a).sum (λ (s : σ a), f a, s⟩))

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

theorem finset.sum_sigma' {β : Type u} {α : Type v} [add_comm_monoid β] {σ : α Type u_1} (s : finset α) (t : Π (a : α), finset (σ a)) (f : Π (a : α), σ a β) :
s.sum (λ (a : α), (t a).sum (λ (s : σ a), f a s)) = (s.sigma t).sum (λ (x : Σ (i : α), σ i), f x.fst x.snd)
theorem finset.prod_sigma' {β : Type u} {α : Type v} [comm_monoid β] {σ : α Type u_1} (s : finset α) (t : Π (a : α), finset (σ a)) (f : Π (a : α), σ a β) :
s.prod (λ (a : α), (t a).prod (λ (s : σ a), f a s)) = (s.sigma t).prod (λ (x : Σ (i : α), σ i), f x.fst x.snd)
theorem finset.sum_bij {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] {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 t ( (a : α) (ha : a s), b = i a ha)) :
s.sum (λ (x : α), f x) = t.sum (λ (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} [comm_monoid β] {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 t ( (a : α) (ha : a s), b = i a ha)) :
s.prod (λ (x : α), f x) = t.prod (λ (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} [add_comm_monoid β] {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) _ = a) (right_inv : (a : γ) (ha : a t), i (j a ha) _ = a) :
s.sum (λ (x : α), f x) = t.sum (λ (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} [comm_monoid β] {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) _ = a) (right_inv : (a : γ) (ha : a t), i (j a ha) _ = a) :
s.prod (λ (x : α), f x) = t.prod (λ (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.prod_comp_finset {ι : Type u_1} {β : Type u} [comm_monoid β] {ι' : Type u_2} [decidable_eq ι] (e : ι ι') (f : ι' β) {s' : finset ι'} {s : finset ι} (h : s = finset.image (e.symm) s') :
s'.prod (λ (i' : ι'), f i') = s.prod (λ (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.equiv.sum_comp_finset {ι : Type u_1} {β : Type u} [add_comm_monoid β] {ι' : Type u_2} [decidable_eq ι] (e : ι ι') (f : ι' β) {s' : finset ι'} {s : finset ι} (h : s = finset.image (e.symm) s') :
s'.sum (λ (i' : ι'), f i') = s.sum (λ (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.sum_finset_product {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] (r : finset × α)) (s : finset γ) (t : γ finset α) (h : (p : γ × α), p r p.fst s p.snd t p.fst) {f : γ × α β} :
r.sum (λ (p : γ × α), f p) = s.sum (λ (c : γ), (t c).sum (λ (a : α), f (c, a)))
theorem finset.prod_finset_product {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] (r : finset × α)) (s : finset γ) (t : γ finset α) (h : (p : γ × α), p r p.fst s p.snd t p.fst) {f : γ × α β} :
r.prod (λ (p : γ × α), f p) = s.prod (λ (c : γ), (t c).prod (λ (a : α), f (c, a)))
theorem finset.sum_finset_product' {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] (r : finset × α)) (s : finset γ) (t : γ finset α) (h : (p : γ × α), p r p.fst s p.snd t p.fst) {f : γ α β} :
r.sum (λ (p : γ × α), f p.fst p.snd) = s.sum (λ (c : γ), (t c).sum (λ (a : α), f c a))
theorem finset.prod_finset_product' {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] (r : finset × α)) (s : finset γ) (t : γ finset α) (h : (p : γ × α), p r p.fst s p.snd t p.fst) {f : γ α β} :
r.prod (λ (p : γ × α), f p.fst p.snd) = s.prod (λ (c : γ), (t c).prod (λ (a : α), f c a))
theorem finset.prod_finset_product_right {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] (r : finset × γ)) (s : finset γ) (t : γ finset α) (h : (p : α × γ), p r p.snd s p.fst t p.snd) {f : α × γ β} :
r.prod (λ (p : α × γ), f p) = s.prod (λ (c : γ), (t c).prod (λ (a : α), f (a, c)))
theorem finset.sum_finset_product_right {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] (r : finset × γ)) (s : finset γ) (t : γ finset α) (h : (p : α × γ), p r p.snd s p.fst t p.snd) {f : α × γ β} :
r.sum (λ (p : α × γ), f p) = s.sum (λ (c : γ), (t c).sum (λ (a : α), f (a, c)))
theorem finset.prod_finset_product_right' {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] (r : finset × γ)) (s : finset γ) (t : γ finset α) (h : (p : α × γ), p r p.snd s p.fst t p.snd) {f : α γ β} :
r.prod (λ (p : α × γ), f p.fst p.snd) = s.prod (λ (c : γ), (t c).prod (λ (a : α), f a c))
theorem finset.sum_finset_product_right' {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] (r : finset × γ)) (s : finset γ) (t : γ finset α) (h : (p : α × γ), p r p.snd s p.fst t p.snd) {f : α γ β} :
r.sum (λ (p : α × γ), f p.fst p.snd) = s.sum (λ (c : γ), (t c).sum (λ (a : α), f a c))
theorem finset.prod_fiberwise_of_maps_to {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] [decidable_eq γ] {s : finset α} {t : finset γ} {g : α γ} (h : (x : α), x s g x t) (f : α β) :
t.prod (λ (y : γ), (finset.filter (λ (x : α), g x = y) s).prod (λ (x : α), f x)) = s.prod (λ (x : α), f x)
theorem finset.sum_fiberwise_of_maps_to {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] [decidable_eq γ] {s : finset α} {t : finset γ} {g : α γ} (h : (x : α), x s g x t) (f : α β) :
t.sum (λ (y : γ), (finset.filter (λ (x : α), g x = y) s).sum (λ (x : α), f x)) = s.sum (λ (x : α), f x)
theorem finset.prod_image' {β : Type u} {α : Type v} {γ : Type w} {f : α β} [comm_monoid β] [decidable_eq α] {s : finset γ} {g : γ α} (h : γ β) (eq : (c : γ), c s f (g c) = (finset.filter (λ (c' : γ), g c' = g c) s).prod (λ (x : γ), h x)) :
(finset.image g s).prod (λ (x : α), f x) = s.prod (λ (x : γ), h x)
theorem finset.sum_image' {β : Type u} {α : Type v} {γ : Type w} {f : α β} [add_comm_monoid β] [decidable_eq α] {s : finset γ} {g : γ α} (h : γ β) (eq : (c : γ), c s f (g c) = (finset.filter (λ (c' : γ), g c' = g c) s).sum (λ (x : γ), h x)) :
(finset.image g s).sum (λ (x : α), f x) = s.sum (λ (x : γ), h x)
theorem finset.prod_mul_distrib {β : Type u} {α : Type v} {s : finset α} {f g : α β} [comm_monoid β] :
s.prod (λ (x : α), f x * g x) = s.prod (λ (x : α), f x) * s.prod (λ (x : α), g x)
theorem finset.sum_add_distrib {β : Type u} {α : Type v} {s : finset α} {f g : α β} [add_comm_monoid β] :
s.sum (λ (x : α), f x + g x) = s.sum (λ (x : α), f x) + s.sum (λ (x : α), g x)
theorem finset.prod_product {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] {s : finset γ} {t : finset α} {f : γ × α β} :
(s ×ˢ t).prod (λ (x : γ × α), f x) = s.prod (λ (x : γ), t.prod (λ (y : α), f (x, y)))
theorem finset.sum_product {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] {s : finset γ} {t : finset α} {f : γ × α β} :
(s ×ˢ t).sum (λ (x : γ × α), f x) = s.sum (λ (x : γ), t.sum (λ (y : α), f (x, y)))
theorem finset.sum_product' {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] {s : finset γ} {t : finset α} {f : γ α β} :
(s ×ˢ t).sum (λ (x : γ × α), f x.fst x.snd) = s.sum (λ (x : γ), t.sum (λ (y : α), f x y))

An uncurried version of finset.sum_product

theorem finset.prod_product' {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] {s : finset γ} {t : finset α} {f : γ α β} :
(s ×ˢ t).prod (λ (x : γ × α), f x.fst x.snd) = s.prod (λ (x : γ), t.prod (λ (y : α), f x y))

An uncurried version of finset.prod_product.

theorem finset.sum_product_right {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] {s : finset γ} {t : finset α} {f : γ × α β} :
(s ×ˢ t).sum (λ (x : γ × α), f x) = t.sum (λ (y : α), s.sum (λ (x : γ), f (x, y)))
theorem finset.prod_product_right {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] {s : finset γ} {t : finset α} {f : γ × α β} :
(s ×ˢ t).prod (λ (x : γ × α), f x) = t.prod (λ (y : α), s.prod (λ (x : γ), f (x, y)))
theorem finset.prod_product_right' {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] {s : finset γ} {t : finset α} {f : γ α β} :
(s ×ˢ t).prod (λ (x : γ × α), f x.fst x.snd) = t.prod (λ (y : α), s.prod (λ (x : γ), f x y))

An uncurried version of finset.prod_product_right.

theorem finset.sum_product_right' {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] {s : finset γ} {t : finset α} {f : γ α β} :
(s ×ˢ t).sum (λ (x : γ × α), f x.fst x.snd) = t.sum (λ (y : α), s.sum (λ (x : γ), f x y))

An uncurried version of finset.prod_product_right

theorem finset.sum_comm' {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] {s : finset γ} {t : γ finset α} {t' : finset α} {s' : α finset γ} (h : (x : γ) (y : α), x s y t x x s' y y t') {f : γ α β} :
s.sum (λ (x : γ), (t x).sum (λ (y : α), f x y)) = t'.sum (λ (y : α), (s' y).sum (λ (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} [comm_monoid β] {s : finset γ} {t : γ finset α} {t' : finset α} {s' : α finset γ} (h : (x : γ) (y : α), x s y t x x s' y y t') {f : γ α β} :
s.prod (λ (x : γ), (t x).prod (λ (y : α), f x y)) = t'.prod (λ (y : α), (s' y).prod (λ (x : γ), f x y))

Generalization of finset.prod_comm to the case when the inner finsets depend on the outer variable.

theorem finset.prod_comm {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] {s : finset γ} {t : finset α} {f : γ α β} :
s.prod (λ (x : γ), t.prod (λ (y : α), f x y)) = t.prod (λ (y : α), s.prod (λ (x : γ), f x y))
theorem finset.sum_comm {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] {s : finset γ} {t : finset α} {f : γ α β} :
s.sum (λ (x : γ), t.sum (λ (y : α), f x y)) = t.sum (λ (y : α), s.sum (λ (x : γ), f x y))
theorem finset.sum_hom_rel {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] [add_comm_monoid γ] {r : β γ Prop} {f : α β} {g : α γ} {s : finset α} (h₁ : r 0 0) (h₂ : (a : α) (b : β) (c : γ), r b c r (f a + b) (g a + c)) :
r (s.sum (λ (x : α), f x)) (s.sum (λ (x : α), g x))
theorem finset.prod_hom_rel {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] [comm_monoid γ] {r : β γ Prop} {f : α β} {g : α γ} {s : finset α} (h₁ : r 1 1) (h₂ : (a : α) (b : β) (c : γ), r b c r (f a * b) (g a * c)) :
r (s.prod (λ (x : α), f x)) (s.prod (λ (x : α), g x))
theorem finset.sum_eq_zero {β : Type u} {α : Type v} [add_comm_monoid β] {f : α β} {s : finset α} (h : (x : α), x s f x = 0) :
s.sum (λ (x : α), f x) = 0
theorem finset.prod_eq_one {β : Type u} {α : Type v} [comm_monoid β] {f : α β} {s : finset α} (h : (x : α), x s f x = 1) :
s.prod (λ (x : α), f x) = 1
theorem finset.sum_subset_zero_on_sdiff {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f g : α β} [add_comm_monoid β] [decidable_eq α] (h : s₁ s₂) (hg : (x : α), x s₂ \ s₁ g x = 0) (hfg : (x : α), x s₁ f x = g x) :
s₁.sum (λ (i : α), f i) = s₂.sum (λ (i : α), g i)
theorem finset.prod_subset_one_on_sdiff {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f g : α β} [comm_monoid β] [decidable_eq α] (h : s₁ s₂) (hg : (x : α), x s₂ \ s₁ g x = 1) (hfg : (x : α), x s₁ f x = g x) :
s₁.prod (λ (i : α), f i) = s₂.prod (λ (i : α), g i)
theorem finset.sum_subset {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α β} [add_comm_monoid β] (h : s₁ s₂) (hf : (x : α), x s₂ x s₁ f x = 0) :
s₁.sum (λ (x : α), f x) = s₂.sum (λ (x : α), f x)
theorem finset.prod_subset {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α β} [comm_monoid β] (h : s₁ s₂) (hf : (x : α), x s₂ x s₁ f x = 1) :
s₁.prod (λ (x : α), f x) = s₂.prod (λ (x : α), f x)
theorem finset.prod_filter_of_ne {β : Type u} {α : Type v} {s : finset α} {f : α β} [comm_monoid β] {p : α Prop} [decidable_pred p] (hp : (x : α), x s f x 1 p x) :
(finset.filter p s).prod (λ (x : α), f x) = s.prod (λ (x : α), f x)
theorem finset.sum_filter_of_ne {β : Type u} {α : Type v} {s : finset α} {f : α β} [add_comm_monoid β] {p : α Prop} [decidable_pred p] (hp : (x : α), x s f x 0 p x) :
(finset.filter p s).sum (λ (x : α), f x) = s.sum (λ (x : α), f x)
theorem finset.prod_filter_ne_one {β : Type u} {α : Type v} {s : finset α} {f : α β} [comm_monoid β] [Π (x : α), decidable (f x 1)] :
(finset.filter (λ (x : α), f x 1) s).prod (λ (x : α), f x) = s.prod (λ (x : α), f x)
theorem finset.sum_filter_ne_zero {β : Type u} {α : Type v} {s : finset α} {f : α β} [add_comm_monoid β] [Π (x : α), decidable (f x 0)] :
(finset.filter (λ (x : α), f x 0) s).sum (λ (x : α), f x) = s.sum (λ (x : α), f x)
theorem finset.prod_filter {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] (p : α Prop) [decidable_pred p] (f : α β) :
(finset.filter p s).prod (λ (a : α), f a) = s.prod (λ (a : α), ite (p a) (f a) 1)
theorem finset.sum_filter {β : Type u} {α : Type v} {s : finset α} [add_comm_monoid β] (p : α Prop) [decidable_pred p] (f : α β) :
(finset.filter p s).sum (λ (a : α), f a) = s.sum (λ (a : α), ite (p a) (f a) 0)
theorem finset.prod_eq_single_of_mem {β : Type u} {α : Type v} [comm_monoid β] {s : finset α} {f : α β} (a : α) (h : a s) (h₀ : (b : α), b s b a f b = 1) :
s.prod (λ (x : α), f x) = f a
theorem finset.sum_eq_single_of_mem {β : Type u} {α : Type v} [add_comm_monoid β] {s : finset α} {f : α β} (a : α) (h : a s) (h₀ : (b : α), b s b a f b = 0) :
s.sum (λ (x : α), f x) = f a
theorem finset.sum_eq_single {β : Type u} {α : Type v} [add_comm_monoid β] {s : finset α} {f : α β} (a : α) (h₀ : (b : α), b s b a f b = 0) (h₁ : a s f a = 0) :
s.sum (λ (x : α), f x) = f a
theorem finset.prod_eq_single {β : Type u} {α : Type v} [comm_monoid β] {s : finset α} {f : α β} (a : α) (h₀ : (b : α), b s b a f b = 1) (h₁ : a s f a = 1) :
s.prod (λ (x : α), f x) = f a
theorem finset.prod_eq_mul_of_mem {β : Type u} {α : Type v} [comm_monoid β] {s : finset α} {f : α β} (a b : α) (ha : a s) (hb : b s) (hn : a b) (h₀ : (c : α), c s c a c b f c = 1) :
s.prod (λ (x : α), f x) = f a * f b
theorem finset.sum_eq_add_of_mem {β : Type u} {α : Type v} [add_comm_monoid β] {s : finset α} {f : α β} (a b : α) (ha : a s) (hb : b s) (hn : a b) (h₀ : (c : α), c s c a c b f c = 0) :
s.sum (λ (x : α), f x) = f a + f b
theorem finset.prod_eq_mul {β : Type u} {α : Type v} [comm_monoid β] {s : finset α} {f : α β} (a b : α) (hn : a b) (h₀ : (c : α), c s c a c b f c = 1) (ha : a s f a = 1) (hb : b s f b = 1) :
s.prod (λ (x : α), f x) = f a * f b
theorem finset.sum_eq_add {β : Type u} {α : Type v} [add_comm_monoid β] {s : finset α} {f : α β} (a b : α) (hn : a b) (h₀ : (c : α), c s c a c b f c = 0) (ha : a s f a = 0) (hb : b s f b = 0) :
s.sum (λ (x : α), f x) = f a + f b
theorem finset.prod_attach {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] {f : α β} :
s.attach.prod (λ (x : {x // x s}), f x) = s.prod (λ (x : α), f x)
theorem finset.sum_attach {β : Type u} {α : Type v} {s : finset α} [add_comm_monoid β] {f : α β} :
s.attach.sum (λ (x : {x // x s}), f x) = s.sum (λ (x : α), f x)
@[simp]
theorem finset.prod_subtype_eq_prod_filter {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] (f : α β) {p : α Prop} [decidable_pred p] :
(finset.subtype p s).prod (λ (x : subtype p), f x) = (finset.filter p s).prod (λ (x : α), f x)

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

@[simp]
theorem finset.sum_subtype_eq_sum_filter {β : Type u} {α : Type v} {s : finset α} [add_comm_monoid β] (f : α β) {p : α Prop} [decidable_pred p] :
(finset.subtype p s).sum (λ (x : subtype p), f x) = (finset.filter p s).sum (λ (x : α), f x)

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

theorem finset.prod_subtype_of_mem {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] (f : α β) {p : α Prop} [decidable_pred p] (h : (x : α), x s p x) :
(finset.subtype p s).prod (λ (x : subtype p), f x) = s.prod (λ (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_of_mem {β : Type u} {α : Type v} {s : finset α} [add_comm_monoid β] (f : α β) {p : α Prop} [decidable_pred p] (h : (x : α), x s p x) :
(finset.subtype p s).sum (λ (x : subtype p), f x) = s.sum (λ (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.sum_subtype_map_embedding {β : Type u} {α : Type v} [add_comm_monoid β] {p : α Prop} {s : finset {x // p x}} {f : {x // p x} β} {g : α β} (h : (x : {x // p x}), x s g x = f x) :
(finset.map (function.embedding.subtype (λ (x : α), p x)) s).sum (λ (x : α), g x) = s.sum (λ (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} [comm_monoid β] {p : α Prop} {s : finset {x // p x}} {f : {x // p x} β} {g : α β} (h : (x : {x // p x}), x s g x = f x) :
(finset.map (function.embedding.subtype (λ (x : α), p x)) s).prod (λ (x : α), g x) = s.prod (λ (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 : finset α) [add_comm_monoid β] (f : s β) :
finset.univ.sum (λ (i : s), f i) = s.attach.sum (λ (i : {x // x s}), f i)
theorem finset.prod_coe_sort_eq_attach {β : Type u} {α : Type v} (s : finset α) [comm_monoid β] (f : s β) :
finset.univ.prod (λ (i : s), f i) = s.attach.prod (λ (i : {x // x s}), f i)
theorem finset.sum_coe_sort {β : Type u} {α : Type v} (s : finset α) (f : α β) [add_comm_monoid β] :
finset.univ.sum (λ (i : s), f i) = s.sum (λ (i : α), f i)
theorem finset.prod_coe_sort {β : Type u} {α : Type v} (s : finset α) (f : α β) [comm_monoid β] :
finset.univ.prod (λ (i : s), f i) = s.prod (λ (i : α), f i)
theorem finset.prod_finset_coe {β : Type u} {α : Type v} [comm_monoid β] (f : α β) (s : finset α) :
finset.univ.prod (λ (i : s), f i) = s.prod (λ (i : α), f i)
theorem finset.sum_finset_coe {β : Type u} {α : Type v} [add_comm_monoid β] (f : α β) (s : finset α) :
finset.univ.sum (λ (i : s), f i) = s.sum (λ (i : α), f i)
theorem finset.prod_subtype {β : Type u} {α : Type v} [comm_monoid β] {p : α Prop} {F : fintype (subtype p)} (s : finset α) (h : (x : α), x s p x) (f : α β) :
s.prod (λ (a : α), f a) = finset.univ.prod (λ (a : subtype p), f a)
theorem finset.sum_subtype {β : Type u} {α : Type v} [add_comm_monoid β] {p : α Prop} {F : fintype (subtype p)} (s : finset α) (h : (x : α), x s p x) (f : α β) :
s.sum (λ (a : α), f a) = finset.univ.sum (λ (a : subtype p), f a)
theorem finset.sum_congr_set {α : Type u_1} [add_comm_monoid α] {β : Type u_2} [fintype β] (s : set β) [decidable_pred (λ (_x : β), _x s)] (f : β α) (g : s α) (w : (x : β) (h : x s), f x = g x, h⟩) (w' : (x : β), x s f x = 0) :

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_1} [comm_monoid α] {β : Type u_2} [fintype β] (s : set β) [decidable_pred (λ (_x : β), _x s)] (f : β α) (g : s α) (w : (x : β) (h : x s), f x = g x, h⟩) (w' : (x : β), x s f x = 1) :

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.prod_apply_dite {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] {s : finset α} {p : α Prop} {hp : decidable_pred p} [decidable_pred (λ (x : α), ¬p x)] (f : Π (x : α), p x γ) (g : Π (x : α), ¬p x γ) (h : γ β) :
s.prod (λ (x : α), h (dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx))) = (finset.filter p s).attach.prod (λ (x : {x // x finset.filter p s}), h (f x.val _)) * (finset.filter (λ (x : α), ¬p x) s).attach.prod (λ (x : {x // x finset.filter (λ (x : α), ¬p x) s}), h (g x.val _))
theorem finset.sum_apply_dite {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] {s : finset α} {p : α Prop} {hp : decidable_pred p} [decidable_pred (λ (x : α), ¬p x)] (f : Π (x : α), p x γ) (g : Π (x : α), ¬p x γ) (h : γ β) :
s.sum (λ (x : α), h (dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx))) = (finset.filter p s).attach.sum (λ (x : {x // x finset.filter p s}), h (f x.val _)) + (finset.filter (λ (x : α), ¬p x) s).attach.sum (λ (x : {x // x finset.filter (λ (x : α), ¬p x) s}), h (g x.val _))
theorem finset.prod_apply_ite {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] {s : finset α} {p : α Prop} {hp : decidable_pred p} (f g : α γ) (h : γ β) :
s.prod (λ (x : α), h (ite (p x) (f x) (g x))) = (finset.filter p s).prod (λ (x : α), h (f x)) * (finset.filter (λ (x : α), ¬p x) s).prod (λ (x : α), h (g x))
theorem finset.sum_apply_ite {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] {s : finset α} {p : α Prop} {hp : decidable_pred p} (f g : α γ) (h : γ β) :
s.sum (λ (x : α), h (ite (p x) (f x) (g x))) = (finset.filter p s).sum (λ (x : α), h (f x)) + (finset.filter (λ (x : α), ¬p x) s).sum (λ (x : α), h (g x))
theorem finset.sum_dite {β : Type u} {α : Type v} [add_comm_monoid β] {s : finset α} {p : α Prop} {hp : decidable_pred p} (f : Π (x : α), p x β) (g : Π (x : α), ¬p x β) :
s.sum (λ (x : α), dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx)) = (finset.filter p s).attach.sum (λ (x : {x // x finset.filter p s}), f x.val _) + (finset.filter (λ (x : α), ¬p x) s).attach.sum (λ (x : {x // x finset.filter (λ (x : α), ¬p x) s}), g x.val _)
theorem finset.prod_dite {β : Type u} {α : Type v} [comm_monoid β] {s : finset α} {p : α Prop} {hp : decidable_pred p} (f : Π (x : α), p x β) (g : Π (x : α), ¬p x β) :
s.prod (λ (x : α), dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx)) = (finset.filter p s).attach.prod (λ (x : {x // x finset.filter p s}), f x.val _) * (finset.filter (λ (x : α), ¬p x) s).attach.prod (λ (x : {x // x finset.filter (λ (x : α), ¬p x) s}), g x.val _)
theorem finset.prod_ite {β : Type u} {α : Type v} [comm_monoid β] {s : finset α} {p : α Prop} {hp : decidable_pred p} (f g : α β) :
s.prod (λ (x : α), ite (p x) (f x) (g x)) = (finset.filter p s).prod (λ (x : α), f x) * (finset.filter (λ (x : α), ¬p x) s).prod (λ (x : α), g x)
theorem finset.sum_ite {β : Type u} {α : Type v} [add_comm_monoid β] {s : finset α} {p : α Prop} {hp : decidable_pred p} (f g : α β) :
s.sum (λ (x : α), ite (p x) (f x) (g x)) = (finset.filter p s).sum (λ (x : α), f x) + (finset.filter (λ (x : α), ¬p x) s).sum (λ (x : α), g x)
theorem finset.prod_ite_of_false {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] {p : α Prop} {hp : decidable_pred p} (f g : α β) (h : (x : α), x s ¬p x) :
s.prod (λ (x : α), ite (p x) (f x) (g x)) = s.prod (λ (x : α), g x)
theorem finset.sum_ite_of_false {β : Type u} {α : Type v} {s : finset α} [add_comm_monoid β] {p : α Prop} {hp : decidable_pred p} (f g : α β) (h : (x : α), x s ¬p x) :
s.sum (λ (x : α), ite (p x) (f x) (g x)) = s.sum (λ (x : α), g x)
theorem finset.prod_ite_of_true {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] {p : α Prop} {hp : decidable_pred p} (f g : α β) (h : (x : α), x s p x) :
s.prod (λ (x : α), ite (p x) (f x) (g x)) = s.prod (λ (x : α), f x)
theorem finset.sum_ite_of_true {β : Type u} {α : Type v} {s : finset α} [add_comm_monoid β] {p : α Prop} {hp : decidable_pred p} (f g : α β) (h : (x : α), x s p x) :
s.sum (λ (x : α), ite (p x) (f x) (g x)) = s.sum (λ (x : α), f x)
theorem finset.sum_apply_ite_of_false {β : Type u} {α : Type v} {γ : Type w} {s : finset α} [add_comm_monoid β] {p : α Prop} {hp : decidable_pred p} (f g : α γ) (k : γ β) (h : (x : α), x s ¬p x) :
s.sum (λ (x : α), k (ite (p x) (f x) (g x))) = s.sum (λ (x : α), k (g x))
theorem finset.prod_apply_ite_of_false {β : Type u} {α : Type v} {γ : Type w} {s : finset α} [comm_monoid β] {p : α Prop} {hp : decidable_pred p} (f g : α γ) (k : γ β) (h : (x : α), x s ¬p x) :
s.prod (λ (x : α), k (ite (p x) (f x) (g x))) = s.prod (λ (x : α), k (g x))
theorem finset.sum_apply_ite_of_true {β : Type u} {α : Type v} {γ : Type w} {s : finset α} [add_comm_monoid β] {p : α Prop} {hp : decidable_pred p} (f g : α γ) (k : γ β) (h : (x : α), x s p x) :
s.sum (λ (x : α), k (ite (p x) (f x) (g x))) = s.sum (λ (x : α), k (f x))
theorem finset.prod_apply_ite_of_true {β : Type u} {α : Type v} {γ : Type w} {s : finset α} [comm_monoid β] {p : α Prop} {hp : decidable_pred p} (f g : α γ) (k : γ β) (h : (x : α), x s p x) :
s.prod (λ (x : α), k (ite (p x) (f x) (g x))) = s.prod (λ (x : α), k (f x))
theorem finset.sum_extend_by_zero {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] (s : finset α) (f : α β) :
s.sum (λ (i : α), ite (i s) (f i) 0) = s.sum (λ (i : α), f i)
theorem finset.prod_extend_by_one {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s : finset α) (f : α β) :
s.prod (λ (i : α), ite (i s) (f i) 1) = s.prod (λ (i : α), f i)
@[simp]
theorem finset.prod_ite_mem {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s t : finset α) (f : α β) :
s.prod (λ (i : α), ite (i t) (f i) 1) = (s t).prod (λ (i : α), f i)
@[simp]
theorem finset.sum_ite_mem {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] (s t : finset α) (f : α β) :
s.sum (λ (i : α), ite (i t) (f i) 0) = (s t).sum (λ (i : α), f i)
@[simp]
theorem finset.sum_dite_eq {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] (s : finset α) (a : α) (b : Π (x : α), a = x β) :
s.sum (λ (x : α), dite (a = x) (λ (h : a = x), b x h) (λ (h : ¬a = x), 0)) = ite (a s) (b a rfl) 0
@[simp]
theorem finset.prod_dite_eq {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s : finset α) (a : α) (b : Π (x : α), a = x β) :
s.prod (λ (x : α), dite (a = x) (λ (h : a = x), b x h) (λ (h : ¬a = x), 1)) = ite (a s) (b a rfl) 1
@[simp]
theorem finset.prod_dite_eq' {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s : finset α) (a : α) (b : Π (x : α), x = a β) :
s.prod (λ (x : α), dite (x = a) (λ (h : x = a), b x h) (λ (h : ¬x = a), 1)) = ite (a s) (b a rfl) 1
@[simp]
theorem finset.sum_dite_eq' {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] (s : finset α) (a : α) (b : Π (x : α), x = a β) :
s.sum (λ (x : α), dite (x = a) (λ (h : x = a), b x h) (λ (h : ¬x = a), 0)) = ite (a s) (b a rfl) 0
@[simp]
theorem finset.prod_ite_eq {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s : finset α) (a : α) (b : α β) :
s.prod (λ (x : α), ite (a = x) (b x) 1) = ite (a s) (b a) 1
@[simp]
theorem finset.sum_ite_eq {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] (s : finset α) (a : α) (b : α β) :
s.sum (λ (x : α), ite (a = x) (b x) 0) = ite (a s) (b a) 0
@[simp]
theorem finset.sum_ite_eq' {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] (s : finset α) (a : α) (b : α β) :
s.sum (λ (x : α), ite (x = a) (b x) 0) = ite (a s) (b a) 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} [comm_monoid β] [decidable_eq α] (s : finset α) (a : α) (b : α β) :
s.prod (λ (x : α), ite (x = a) (b x) 1) = ite (a s) (b a) 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} [add_comm_monoid β] (p : Prop) [decidable p] (s t : finset α) (f : α β) :
(ite p s t).sum (λ (x : α), f x) = ite p (s.sum (λ (x : α), f x)) (t.sum (λ (x : α), f x))
theorem finset.prod_ite_index {β : Type u} {α : Type v} [comm_monoid β] (p : Prop) [decidable p] (s t : finset α) (f : α β) :
(ite p s t).prod (λ (x : α), f x) = ite p (s.prod (λ (x : α), f x)) (t.prod (λ (x : α), f x))
@[simp]
theorem finset.sum_ite_irrel {β : Type u} {α : Type v} [add_comm_monoid β] (p : Prop) [decidable p] (s : finset α) (f g : α β) :
s.sum (λ (x : α), ite p (f x) (g x)) = ite p (s.sum (λ (x : α), f x)) (s.sum (λ (x : α), g x))
@[simp]
theorem finset.prod_ite_irrel {β : Type u} {α : Type v} [comm_monoid β] (p : Prop) [decidable p] (s : finset α) (f g : α β) :
s.prod (λ (x : α), ite p (f x) (g x)) = ite p (s.prod (λ (x : α), f x)) (s.prod (λ (x : α), g x))
@[simp]
theorem finset.sum_dite_irrel {β : Type u} {α : Type v} [add_comm_monoid β] (p : Prop) [decidable p] (s : finset α) (f : p α β) (g : ¬p α β) :
s.sum (λ (x : α), dite p (λ (h : p), f h x) (λ (h : ¬p), g h x)) = dite p (λ (h : p), s.sum (λ (x : α), f h x)) (λ (h : ¬p), s.sum (λ (x : α), g h x))
@[simp]
theorem finset.prod_dite_irrel {β : Type u} {α : Type v} [comm_monoid β] (p : Prop) [decidable p] (s : finset α) (f : p α β) (g : ¬p α β) :
s.prod (λ (x : α), dite p (λ (h : p), f h x) (λ (h : ¬p), g h x)) = dite p (λ (h : p), s.prod (λ (x : α), f h x)) (λ (h : ¬p), s.prod (λ (x : α), g h x))
@[simp]
theorem finset.prod_pi_mul_single' {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (a : α) (x : β) (s : finset α) :
s.prod (λ (a' : α), pi.mul_single a x a') = ite (a s) x 1
@[simp]
theorem finset.sum_pi_single' {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] (a : α) (x : β) (s : finset α) :
s.sum (λ (a' : α), pi.single a x a') = ite (a s) x 0
@[simp]
theorem finset.sum_pi_single {α : Type v} {β : α Type u_1} [decidable_eq α] [Π (a : α), add_comm_monoid (β a)] (a : α) (f : Π (a : α), β a) (s : finset α) :
s.sum (λ (a' : α), pi.single a' (f a') a) = ite (a s) (f a) 0
@[simp]
theorem finset.prod_pi_mul_single {α : Type v} {β : α Type u_1} [decidable_eq α] [Π (a : α), comm_monoid (β a)] (a : α) (f : Π (a : α), β a) (s : finset α) :
s.prod (λ (a' : α), pi.mul_single a' (f a') a) = ite (a s) (f a) 1
theorem finset.prod_bij_ne_one {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] {s : finset α} {t : finset γ} {f : α β} {g : γ β} (i : Π (a : α), a s f a 1 γ) (hi : (a : α) (h₁ : a s) (h₂ : f a 1), i a h₁ h₂ t) (i_inj : (a₁ 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 t g b 1 ( (a : α) (h₁ : a s) (h₂ : f a 1), b = i a h₁ h₂)) (h : (a : α) (h₁ : a s) (h₂ : f a 1), f a = g (i a h₁ h₂)) :
s.prod (λ (x : α), f x) = t.prod (λ (x : γ), g x)
theorem finset.sum_bij_ne_zero {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] {s : finset α} {t : finset γ} {f : α β} {g : γ β} (i : Π (a : α), a s f a 0 γ) (hi : (a : α) (h₁ : a s) (h₂ : f a 0), i a h₁ h₂ t) (i_inj : (a₁ 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 t g b 0 ( (a : α) (h₁ : a s) (h₂ : f a 0), b = i a h₁ h₂)) (h : (a : α) (h₁ : a s) (h₂ : f a 0), f a = g (i a h₁ h₂)) :
s.sum (λ (x : α), f x) = t.sum (λ (x : γ), g x)
theorem finset.sum_dite_of_false {β : Type u} {α : Type v} {s : finset α} [add_comm_monoid β] {p : α Prop} {hp : decidable_pred p} (h : (x : α), x s ¬p x) (f : Π (x : α), p x β) (g : Π (x : α), ¬p x β) :
s.sum (λ (x : α), dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx)) = finset.univ.sum (λ (x : s), g x.val _)
theorem finset.prod_dite_of_false {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] {p : α Prop} {hp : decidable_pred p} (h : (x : α), x s ¬p x) (f : Π (x : α), p x β) (g : Π (x : α), ¬p x β) :
s.prod (λ (x : α), dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx)) = finset.univ.prod (λ (x : s), g x.val _)
theorem finset.sum_dite_of_true {β : Type u} {α : Type v} {s : finset α} [add_comm_monoid β] {p : α Prop} {hp : decidable_pred p} (h : (x : α), x s p x) (f : Π (x : α), p x β) (g : Π (x : α), ¬p x β) :
s.sum (λ (x : α), dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx)) = finset.univ.sum (λ (x : s), f x.val _)
theorem finset.prod_dite_of_true {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] {p : α Prop} {hp : decidable_pred p} (h : (x : α), x s p x) (f : Π (x : α), p x β) (g : Π (x : α), ¬p x β) :
s.prod (λ (x : α), dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx)) = finset.univ.prod (λ (x : s), f x.val _)
theorem finset.nonempty_of_sum_ne_zero {β : Type u} {α : Type v} {s : finset α} {f : α β} [add_comm_monoid β] (h : s.sum (λ (x : α), f x) 0) :
theorem finset.nonempty_of_prod_ne_one {β : Type u} {α : Type v} {s : finset α} {f : α β} [comm_monoid β] (h : s.prod (λ (x : α), f x) 1) :
theorem finset.exists_ne_zero_of_sum_ne_zero {β : Type u} {α : Type v} {s : finset α} {f : α β} [add_comm_monoid β] (h : s.sum (λ (x : α), f x) 0) :
(a : α) (H : a s), f a 0
theorem finset.exists_ne_one_of_prod_ne_one {β : Type u} {α : Type v} {s : finset α} {f : α β} [comm_monoid β] (h : s.prod (λ (x : α), f x) 1) :
(a : α) (H : a s), f a 1
theorem finset.prod_range_succ_comm {β : Type u} [comm_monoid β] (f : β) (n : ) :
(finset.range (n + 1)).prod (λ (x : ), f x) = f n * (finset.range n).prod (λ (x : ), f x)
theorem finset.sum_range_succ_comm {β : Type u} [add_comm_monoid β] (f : β) (n : ) :
(finset.range (n + 1)).sum (λ (x : ), f x) = f n + (finset.range n).sum (λ (x : ), f x)
theorem finset.prod_range_succ {β : Type u} [comm_monoid β] (f : β) (n : ) :
(finset.range (n + 1)).prod (λ (x : ), f x) = (finset.range n).prod (λ (x : ), f x) * f n
theorem finset.sum_range_succ {β : Type u} [add_comm_monoid β] (f : β) (n : ) :
(finset.range (n + 1)).sum (λ (x : ), f x) = (finset.range n).sum (λ (x : ), f x) + f n
theorem finset.prod_range_succ' {β : Type u} [comm_monoid β] (f : β) (n : ) :
(finset.range (n + 1)).prod (λ (k : ), f k) = (finset.range n).prod (λ (k : ), f (k + 1)) * f 0
theorem finset.sum_range_succ' {β : Type u} [add_comm_monoid β] (f : β) (n : ) :
(finset.range (n + 1)).sum (λ (k : ), f k) = (finset.range n).sum (λ (k : ), f (k + 1)) + f 0
theorem finset.eventually_constant_sum {β : Type u} [add_comm_monoid β] {u : β} {N : } (hu : (n : ), n N u n = 0) {n : } (hn : N n) :
(finset.range (n + 1)).sum (λ (k : ), u k) = (finset.range (N + 1)).sum (λ (k : ), u k)
theorem finset.eventually_constant_prod {β : Type u} [comm_monoid β] {u : β} {N : } (hu : (n : ), n N u n = 1) {n : } (hn : N n) :
(finset.range (n + 1)).prod (λ (k : ), u k) = (finset.range (N + 1)).prod (λ (k : ), u k)
theorem finset.prod_range_add {β : Type u} [comm_monoid β] (f : β) (n m : ) :
(finset.range (n + m)).prod (λ (x : ), f x) = (finset.range n).prod (λ (x : ), f x) * (finset.range m).prod (λ (x : ), f (n + x))
theorem finset.sum_range_add {β : Type u} [add_comm_monoid β] (f : β) (n m : ) :
(finset.range (n + m)).sum (λ (x : ), f x) = (finset.range n).sum (λ (x : ), f x) + (finset.range m).sum (λ (x : ), f (n + x))
theorem finset.sum_range_add_sub_sum_range {α : Type u_1} [add_comm_group α] (f : α) (n m : ) :
(finset.range (n + m)).sum (λ (k : ), f k) - (finset.range n).sum (λ (k : ), f k) = (finset.range m).sum (λ (k : ), f (n + k))
theorem finset.prod_range_add_div_prod_range {α : Type u_1} [comm_group α] (f : α) (n m : ) :
(finset.range (n + m)).prod (λ (k : ), f k) / (finset.range n).prod (λ (k : ), f k) = (finset.range m).prod (λ (k : ), f (n + k))
theorem finset.sum_range_zero {β : Type u} [add_comm_monoid β] (f : β) :
(finset.range 0).sum (λ (k : ), f k) = 0
theorem finset.prod_range_zero {β : Type u} [comm_monoid β] (f : β) :
(finset.range 0).prod (λ (k : ), f k) = 1
theorem finset.sum_range_one {β : Type u} [add_comm_monoid β] (f : β) :
(finset.range 1).sum (λ (k : ), f k) = f 0
theorem finset.prod_range_one {β : Type u} [comm_monoid β] (f : β) :
(finset.range 1).prod (λ (k : ), f k) = f 0
theorem finset.sum_list_map_count {α : Type v} [decidable_eq α] (l : list α) {M : Type u_1} [add_comm_monoid M] (f : α M) :
(list.map f l).sum = l.to_finset.sum (λ (m : α), list.count m l f m)
theorem finset.prod_list_map_count {α : Type v} [decidable_eq α] (l : list α) {M : Type u_1} [comm_monoid M] (f : α M) :
(list.map f l).prod = l.to_finset.prod (λ (m : α), f m ^ list.count m l)
theorem finset.sum_list_count {α : Type v} [decidable_eq α] [add_comm_monoid α] (s : list α) :
s.sum = s.to_finset.sum (λ (m : α), list.count m s m)
theorem finset.prod_list_count {α : Type v} [decidable_eq α] [comm_monoid α] (s : list α) :
s.prod = s.to_finset.prod (λ (m : α), m ^ list.count m s)
theorem finset.prod_list_count_of_subset {α : Type v} [decidable_eq α] [comm_monoid α] (m : list α) (s : finset α) (hs : m.to_finset s) :
m.prod = s.prod (λ (i : α), i ^ list.count i m)
theorem finset.sum_list_count_of_subset {α : Type v} [decidable_eq α] [add_comm_monoid α] (m : list α) (s : finset α) (hs : m.to_finset s) :
m.sum = s.sum (λ (i : α), list.count i m i)
theorem finset.sum_filter_count_eq_countp {α : Type v} [decidable_eq α] (p : α Prop) [decidable_pred p] (l : list α) :
(finset.filter p l.to_finset).sum (λ (x : α), list.count x l) = list.countp p l
theorem finset.prod_multiset_map_count {α : Type v} [decidable_eq α] (s : multiset α) {M : Type u_1} [comm_monoid M] (f : α M) :
(multiset.map f s).prod = s.to_finset.prod (λ (m : α), f m ^ multiset.count m s)
theorem finset.sum_multiset_map_count {α : Type v} [decidable_eq α] (s : multiset α) {M : Type u_1} [add_comm_monoid M] (f : α M) :
(multiset.map f s).sum = s.to_finset.sum (λ (m : α), multiset.count m s f m)
theorem finset.sum_multiset_count {α : Type v} [decidable_eq α] [add_comm_monoid α] (s : multiset α) :
s.sum = s.to_finset.sum (λ (m : α), multiset.count m s m)
theorem finset.prod_multiset_count {α : Type v} [decidable_eq α] [comm_monoid α] (s : multiset α) :
s.prod = s.to_finset.prod (λ (m : α), m ^ multiset.count m s)
theorem finset.prod_multiset_count_of_subset {α : Type v} [decidable_eq α] [comm_monoid α] (m : multiset α) (s : finset α) (hs : m.to_finset s) :
m.prod = s.prod (λ (i : α), i ^ multiset.count i m)
theorem finset.sum_multiset_count_of_subset {α : Type v} [decidable_eq α] [add_comm_monoid α] (m : multiset α) (s : finset α) (hs : m.to_finset s) :
m.sum = s.sum (λ (i : α), multiset.count i m i)
theorem finset.sum_mem_multiset {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] (m : multiset α) (f : {x // x m} β) (g : α β) (hfg : (x : {x // x m}), f x = g x) :
finset.univ.sum (λ (x : {x // x m}), f x) = m.to_finset.sum (λ (x : α), g x)
theorem finset.prod_mem_multiset {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (m : multiset α) (f : {x // x m} β) (g : α β) (hfg : (x : {x // x m}), f x = g x) :
finset.univ.prod (λ (x : {x // x m}), f x) = m.to_finset.prod (λ (x : α), g x)
theorem finset.prod_induction {α : Type v} {s : finset α} {M : Type u_1} [comm_monoid M] (f : α M) (p : M Prop) (p_mul : (a b : M), p a p b p (a * b)) (p_one : p 1) (p_s : (x : α), x s p (f x)) :
p (s.prod (λ (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 {α : Type v} {s : finset α} {M : Type u_1} [add_comm_monoid M] (f : α M) (p : M Prop) (p_mul : (a b : M), p a p b p (a + b)) (p_one : p 0) (p_s : (x : α), x s p (f x)) :
p (s.sum (λ (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.sum_induction_nonempty {α : Type v} {s : finset α} {M : Type u_1} [add_comm_monoid M] (f : α M) (p : M Prop) (p_mul : (a b : M), p a p b p (a + b)) (hs_nonempty : s.nonempty) (p_s : (x : α), x s p (f x)) :
p (s.sum (λ (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} [comm_monoid M] (f : α M) (p : M Prop) (p_mul : (a b : M), p a p b p (a * b)) (hs_nonempty : s.nonempty) (p_s : (x : α), x s p (f x)) :
p (s.prod (λ (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.prod_range_induction {β : Type u} [comm_monoid β] (f s : β) (h0 : s 0 = 1) (h : (n : ), s (n + 1) = s n * f n) (n : ) :
(finset.range n).prod (λ (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_induction {β : Type u} [add_comm_monoid β] (f s : β) (h0 : s 0 = 0) (h : (n : ), s (n + 1) = s n + f n) (n : ) :
(finset.range n).sum (λ (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.sum_range_sub {M : Type u_1} [add_comm_group M] (f : M) (n : ) :
(finset.range n).sum (λ (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} [comm_group M] (f : M) (n : ) :
(finset.range n).prod (λ (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.prod_range_div' {M : Type u_1} [comm_group M] (f : M) (n : ) :
(finset.range n).prod (λ (i : ), f i / f (i + 1)) = f 0 / f n
theorem finset.sum_range_sub' {M : Type u_1} [add_comm_group M] (f : M) (n : ) :
(finset.range n).sum (λ (i : ), f i - f (i + 1)) = f 0 - f n
theorem finset.eq_prod_range_div {M : Type u_1} [comm_group M] (f : M) (n : ) :
f n = f 0 * (finset.range n).prod (λ (i : ), f (i + 1) / f i)
theorem finset.eq_sum_range_sub {M : Type u_1} [add_comm_group M] (f : M) (n : ) :
f n = f 0 + (finset.range n).sum (λ (i : ), f (i + 1) - f i)
theorem finset.eq_prod_range_div' {M : Type u_1} [comm_group M] (f : M) (n : ) :
f n = (finset.range (n + 1)).prod (λ (i : ), ite (i = 0) (f 0) (f i / f (i - 1)))
theorem finset.eq_sum_range_sub' {M : Type u_1} [add_comm_group M] (f : M) (n : ) :
f n = (finset.range (n + 1)).sum (λ (i : ), ite (i = 0) (f 0) (f i - f (i - 1)))
theorem finset.sum_range_tsub {α : Type v} [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] [contravariant_class α α has_add.add has_le.le] {f : α} (h : monotone f) (n : ) :
(finset.range n).sum (λ (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.prod_const {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] (b : β) :
s.prod (λ (x : α), b) = b ^ s.card
@[simp]
theorem finset.sum_const {β : Type u} {α : Type v} {s : finset α} [add_comm_monoid β] (b : β) :
s.sum (λ (x : α), b) = s.card b
theorem finset.sum_eq_card_nsmul {β : Type u} {α : Type v} {s : finset α} {f : α β} [add_comm_monoid β] {b : β} (hf : (a : α), a s f a = b) :
s.sum (λ (a : α), f a) = s.card b
theorem finset.prod_eq_pow_card {β : Type u} {α : Type v} {s : finset α} {f : α β} [comm_monoid β] {b : β} (hf : (a : α), a s f a = b) :
s.prod (λ (a : α), f a) = b ^ s.card
theorem finset.nsmul_eq_sum_const {β : Type u} [add_comm_monoid β] (b : β) (n : ) :
n b = (finset.range n).sum (λ (k : ), b)
theorem finset.pow_eq_prod_const {β : Type u} [comm_monoid β] (b : β) (n : ) :
b ^ n = (finset.range n).prod (λ (k : ), b)
theorem finset.sum_nsmul {β : Type u} {α : Type v} [add_comm_monoid β] (s : finset α) (n : ) (f : α β) :
s.sum (λ (x : α), n f x) = n s.sum (λ (x : α), f x)
theorem finset.prod_pow {β : Type u} {α : Type v} [comm_monoid β] (s : finset α) (n : ) (f : α β) :
s.prod (λ (x : α), f x ^ n) = s.prod (λ (x : α), f x) ^ n
theorem finset.prod_flip {β : Type u} [comm_monoid β] {n : } (f : β) :
(finset.range (n + 1)).prod (λ (r : ), f (n - r)) = (finset.range (n + 1)).prod (λ (k : ), f k)
theorem finset.sum_flip {β : Type u} [add_comm_monoid β] {n : } (f : β) :
(finset.range (n + 1)).sum (λ (r : ), f (n - r)) = (finset.range (n + 1)).sum (λ (k : ), f k)
theorem finset.prod_involution {β : Type u} {α : Type v} [comm_monoid β] {s : finset α} {f : α β} (g : Π (a : α), a s α) (h : (a : α) (ha : a s), f a * f (g a ha) = 1) (g_ne : (a : α) (ha : a s), f a 1 g a ha a) (g_mem : (a : α) (ha : a s), g a ha s) (g_inv : (a : α) (ha : a s), g (g a ha) _ = a) :
s.prod (λ (x : α), f x) = 1
theorem finset.sum_involution {β : Type u} {α : Type v} [add_comm_monoid β] {s : finset α} {f : α β} (g : Π (a : α), a s α) (h : (a : α) (ha : a s), f a + f (g a ha) = 0) (g_ne : (a : α) (ha : a s), f a 0 g a ha a) (g_mem : (a : α) (ha : a s), g a ha s) (g_inv : (a : α) (ha : a s), g (g a ha) _ = a) :
s.sum (λ (x : α), f x) = 0
theorem finset.prod_comp {β : Type u} {α : Type v} {γ : Type w} {s : finset α} [comm_monoid β] [decidable_eq γ] (f : γ β) (g : α γ) :
s.prod (λ (a : α), f (g a)) = (finset.image g s).prod (λ (b : γ), f b ^ (finset.filter (λ (a : α), g a = b) s).card)

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

theorem finset.sum_comp {β : Type u} {α : Type v} {γ : Type w} {s : finset α} [add_comm_monoid β] [decidable_eq γ] (f : γ β) (g : α γ) :
s.sum (λ (a : α), f (g a)) = (finset.image g s).sum (λ (b : γ), (finset.filter (λ (a : α), g a = b) s).card f b)

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

theorem finset.sum_piecewise {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] (s t : finset α) (f g : α β) :
s.sum (λ (x : α), t.piecewise f g x) = (s t).sum (λ (x : α), f x) + (s \ t).sum (λ (x : α), g x)
theorem finset.prod_piecewise {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s t : finset α) (f g : α β) :
s.prod (λ (x : α), t.piecewise f g x) = (s t).prod (λ (x : α), f x) * (s \ t).prod (λ (x : α), g x)
theorem finset.prod_inter_mul_prod_diff {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s t : finset α) (f : α β) :
(s t).prod (λ (x : α), f x) * (s \ t).prod (λ (x : α), f x) = s.prod (λ (x : α), f x)
theorem finset.sum_inter_add_sum_diff {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] (s t : finset α) (f : α β) :
(s t).sum (λ (x : α), f x) + (s \ t).sum (λ (x : α), f x) = s.sum (λ (x : α), f x)
theorem finset.prod_eq_mul_prod_diff_singleton {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α β) :
s.prod (λ (x : α), f x) = f i * (s \ {i}).prod (λ (x : α), f x)
theorem finset.sum_eq_add_sum_diff_singleton {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α β) :
s.sum (λ (x : α), f x) = f i + (s \ {i}).sum (λ (x : α), f x)
theorem finset.prod_eq_prod_diff_singleton_mul {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α β) :
s.prod (λ (x : α), f x) = (s \ {i}).prod (λ (x : α), f x) * f i
theorem finset.sum_eq_sum_diff_singleton_add {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α β) :
s.sum (λ (x : α), f x) = (s \ {i}).sum (λ (x : α), f x) + f i
theorem fintype.prod_eq_mul_prod_compl {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] [fintype α] (a : α) (f : α β) :
finset.univ.prod (λ (i : α), f i) = f a * {a}.prod (λ (i : α), f i)
theorem fintype.sum_eq_add_sum_compl {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] [fintype α] (a : α) (f : α β) :
finset.univ.sum (λ (i : α), f i) = f a + {a}.sum (λ (i : α), f i)
theorem fintype.prod_eq_prod_compl_mul {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] [fintype α] (a : α) (f : α β) :
finset.univ.prod (λ (i : α), f i) = {a}.prod (λ (i : α), f i) * f a
theorem fintype.sum_eq_sum_compl_add {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] [fintype α] (a : α) (f : α β) :
finset.univ.sum (λ (i : α), f i) = {a}.sum (λ (i : α), f i) + f a
theorem finset.dvd_prod_of_mem {β : Type u} {α : Type v} [comm_monoid β] (f : α β) {a : α} {s : finset α} (ha : a s) :
f a s.prod (λ (i : α), f i)
theorem finset.sum_partition {β : Type u} {α : Type v} {s : finset α} {f : α β} [add_comm_monoid β] (R : setoid α) [decidable_rel setoid.r] :
s.sum (λ (x : α), f x) = (finset.image quotient.mk s).sum (λ (xbar : quotient R), (finset.filter (λ (y : α), y = xbar) s).sum (λ (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 : α β} [comm_monoid β] (R : setoid α) [decidable_rel setoid.r] :
s.prod (λ (x : α), f x) = (finset.image quotient.mk s).prod (λ (xbar : quotient R), (finset.filter (λ (y : α), y = xbar) s).prod (λ (y : α), f y))

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

theorem finset.prod_cancels_of_partition_cancels {β : Type u} {α : Type v} {s : finset α} {f : α β} [comm_monoid β] (R : setoid α) [decidable_rel setoid.r] (h : (x : α), x s (finset.filter (λ (y : α), y x) s).prod (λ (a : α), f a) = 1) :
s.prod (λ (x : α), f x) = 1

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

theorem finset.sum_cancels_of_partition_cancels {β : Type u} {α : Type v} {s : finset α} {f : α β} [add_comm_monoid β] (R : setoid α) [decidable_rel setoid.r] (h : (x : α), x s (finset.filter (λ (y : α), y x) s).sum (λ (a : α), f a) = 0) :
s.sum (λ (x : α), f x) = 0

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

theorem finset.prod_update_of_not_mem {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α β) (b : β) :
s.prod (λ (x : α), function.update f i b x) = s.prod (λ (x : α), f x)
theorem finset.sum_update_of_not_mem {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α β) (b : β) :
s.sum (λ (x : α), function.update f i b x) = s.sum (λ (x : α), f x)
theorem finset.prod_update_of_mem {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α β) (b : β) :
s.prod (λ (x : α), function.update f i b x) = b * (s \ {i}).prod (λ (x : α), f x)
theorem finset.sum_update_of_mem {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α β) (b : β) :
s.sum (λ (x : α), function.update f i b x) = b + (s \ {i}).sum (λ (x : α), f x)
theorem finset.eq_of_card_le_one_of_sum_eq {β : Type u} {α : Type v} [add_comm_monoid β] {s : finset α} (hc : s.card 1) {f : α β} {b : β} (h : s.sum (λ (x : α), f x) = b) (x : α) (H : x s) :
f x = b

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

theorem finset.eq_of_card_le_one_of_prod_eq {β : Type u} {α : Type v} [comm_monoid β] {s : finset α} (hc : s.card 1) {f : α β} {b : β} (h : s.prod (λ (x : α), f x) = b) (x : α) (H : x s) :
f x = b

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

theorem finset.add_sum_erase {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] (s : finset α) (f : α β) {a : α} (h : a s) :
f a + (s.erase a).sum (λ (x : α), f x) = s.sum (λ (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} [comm_monoid β] [decidable_eq α] (s : finset α) (f : α β) {a : α} (h : a s) :
f a * (s.erase a).prod (λ (x : α), f x) = s.prod (λ (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} [add_comm_monoid β] [decidable_eq α] (s : finset α) (f : α β) {a : α} (h : a s) :
(s.erase a).sum (λ (x : α), f x) + f a = s.sum (λ (x : α), f x)

A variant of finset.add_sum_erase with the addition swapped.

theorem finset.prod_erase_mul {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s : finset α) (f : α β) {a : α} (h : a s) :
(s.erase a).prod (λ (x : α), f x) * f a = s.prod (λ (x : α), f x)

A variant of finset.mul_prod_erase with the multiplication swapped.

theorem finset.prod_erase {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s : finset α) {f : α β} {a : α} (h : f a = 1) :
(s.erase a).prod (λ (x : α), f x) = s.prod (λ (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_erase {β : Type u} {α : Type v} [add_comm_monoid β] [decidable_eq α] (s : finset α) {f : α β} {a : α} (h : f a = 0) :
(s.erase a).sum (λ (x : α), f x) = s.sum (λ (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_ite_one {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] {f : α Prop} [decidable_pred f] (hf : s.pairwise_disjoint f) (a : β) :
s.prod (λ (i : α), ite (f i) a 1) = ite ( (i : α) (H : i s), f i) a 1

See also finset.prod_boole.

theorem finset.sum_ite_zero {β : Type u} {α : Type v} {s : finset α} [add_comm_monoid β] {f : α Prop} [decidable_pred f] (hf : s.pairwise_disjoint f) (a : β) :
s.sum (λ (i : α), ite (f i) a 0) = ite ( (i : α) (H : i s), f i) a 0

See also finset.sum_boole.

theorem finset.sum_erase_lt_of_pos {α : Type v} {γ : Type u_1} [decidable_eq α] [ordered_add_comm_monoid γ] [covariant_class γ γ has_add.add has_lt.lt] {s : finset α} {d : α} (hd : d s) {f : α γ} (hdf : 0 < f d) :
(s.erase d).sum (λ (m : α), f m) < s.sum (λ (m : α), f m)
theorem finset.prod_erase_lt_of_one_lt {α : Type v} {γ : Type u_1} [decidable_eq α] [ordered_comm_monoid γ] [covariant_class γ γ has_mul.mul has_lt.lt] {s : finset α} {d : α} (hd : d s) {f : α γ} (hdf : 1 < f d) :
(s.erase d).prod (λ (m : α), f m) < s.prod (λ (m : α), f m)
theorem finset.eq_zero_of_sum_eq_zero {β : Type u} {α : Type v} [add_comm_monoid β] {s : finset α} {f : α β} {a : α} (hp : s.sum (λ (x : α), f x) = 0) (h1 : (x : α), x s x a f x = 0) (x : α) (H : x s) :
f x = 0

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

theorem finset.eq_one_of_prod_eq_one {β : Type u} {α : Type v} [comm_monoid β] {s : finset α} {f : α β} {a : α} (hp : s.prod (λ (x : α), f x) = 1) (h1 : (x : α), x s x a f x = 1) (x : α) (H : x s) :
f x = 1

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

theorem finset.prod_pow_boole {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s : finset α) (f : α β) (a : α) :
s.prod (λ (x : α), f x ^ ite (a = x) 1 0) = ite (a s) (f a) 1
theorem finset.prod_dvd_prod_of_dvd {β : Type u} {α : Type v} [comm_monoid β] {S : finset α} (g1 g2 : α β) (h : (a : α), a S g1 a g2 a) :
S.prod g1 S.prod g2
theorem finset.prod_dvd_prod_of_subset {ι : Type u_1} {M : Type u_2} [comm_monoid M] (s t : finset ι) (f : ι M) (h : s t) :
s.prod (λ (i : ι), f i) t.prod (λ (i : ι), f i)
theorem finset.prod_add_prod_eq {β : Type u} {α : Type v} [comm_semiring β] {s : finset α} {i : α} {f g h : α β} (hi : i s) (h1 : g i + h i = f i) (h2 : (j : α), j s j i g j = f j) (h3 : (j : α), j s j i h j = f j) :
s.prod (λ (i : α), g i) + s.prod (λ (i : α), h i) = s.prod (λ (i : α), f i)

If f = g = h everywhere but at i, where f i = g i + h i, then the product of f over s is the sum of the products of g and h.

theorem finset.card_eq_sum_ones {α : Type v} (s : finset α) :
s.card = s.sum (λ (_x : α), 1)
theorem finset.sum_const_nat {α : Type v} {s : finset α} {m : } {f : α } (h₁ : (x : α), x s f x = m) :
s.sum (λ (x : α), f x) = s.card * m
@[simp]
theorem finset.sum_boole {β : Type u} {α : Type v} {s : finset α} {p : α Prop} [non_assoc_semiring β] {hp : decidable_pred p} :
s.sum (λ (x : α), ite (p x) 1 0) = ((finset.filter p s).card)
theorem commute.sum_right {β : Type u} {α : Type v} [non_unital_non_assoc_semiring β] (s : finset α) (f : α β) (b : β) (h : (i : α), i s commute b (f i)) :
commute b (s.sum (λ (i : α), f i))
theorem commute.sum_left {β : Type u} {α : Type v} [non_unital_non_assoc_semiring β] (s : finset α) (f : α β) (b : β) (h : (i : α), i s commute (f i) b) :
commute (s.sum (λ (i : α), f i)) b
@[simp]
theorem finset.op_sum {β : Type u} {α : Type v} [add_comm_monoid β] {s : finset α} (f : α β) :
mul_opposite.op (s.sum (λ (x : α), f x)) = s.sum (λ (x : α), mul_opposite.op (f x))

Moving to the opposite additive commutative monoid commutes with summing.

@[simp]
theorem finset.unop_sum {β : Type u} {α : Type v} [add_comm_monoid β] {s : finset α} (f : α βᵐᵒᵖ) :
mul_opposite.unop (s.sum (λ (x : α), f x)) = s.sum (λ (x : α), mul_opposite.unop (f x))
@[simp]
theorem finset.sum_neg_distrib {β : Type u} {α : Type v} {s : finset α} {f : α β} [subtraction_comm_monoid β] :
s.sum (λ (x : α), -f x) = -s.sum (λ (x : α), f x)
@[simp]
theorem finset.prod_inv_distrib {β : Type u} {α : Type v} {s : finset α} {f : α β} [division_comm_monoid β] :
s.prod (λ (x : α), (f x)⁻¹) = (s.prod (λ (x : α), f x))⁻¹
@[simp]
theorem finset.sum_sub_distrib {β : Type u} {α : Type v} {s : finset α} {f g : α β} [subtraction_comm_monoid β] :
s.sum (λ (x : α), f x - g x) = s.sum (λ (x : α), f x) - s.sum (λ (x : α), g x)
@[simp]
theorem finset.prod_div_distrib {β : Type u} {α : Type v} {s : finset α} {f g : α β} [division_comm_monoid β] :
s.prod (λ (x : α), f x / g x) = s.prod (λ (x : α), f x) / s.prod (λ (x : α), g x)
theorem finset.sum_zsmul {β : Type u} {α : Type v} [subtraction_comm_monoid β] (f : α β) (s : finset α) (n : ) :
s.sum (λ (a : α), n f a) = n s.sum (λ (a : α), f a)
theorem finset.prod_zpow {β : Type u} {α : Type v} [division_comm_monoid β] (f : α β) (s : finset α) (n : ) :
s.prod (λ (a : α), f a ^ n) = s.prod (λ (a : α), f a) ^ n
@[simp]
theorem finset.sum_sdiff_eq_sub {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α β} [add_comm_group β] [decidable_eq α] (h : s₁ s₂) :
(s₂ \ s₁).sum (λ (x : α), f x) = s₂.sum (λ (x : α), f x) - s₁.sum (λ (x : α), f x)
@[simp]
theorem finset.prod_sdiff_eq_div {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α β} [comm_group β] [decidable_eq α] (h : s₁ s₂) :
(s₂ \ s₁).prod (λ (x : α), f x) = s₂.prod (λ (x : α), f x) / s₁.prod (λ (x : α), f x)
theorem finset.prod_sdiff_div_prod_sdiff {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α β} [comm_group β] [decidable_eq α] :
(s₂ \ s₁).prod (λ (x : α), f x) / (s₁ \ s₂).prod (λ (x : α), f x) = s₂.prod (λ (x : α), f x) / s₁.prod (λ (x : α), f x)
theorem finset.sum_sdiff_sub_sum_sdiff {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α β} [add_comm_group β] [decidable_eq α] :
(s₂ \ s₁).sum (λ (x : α), f x) - (s₁ \ s₂).sum (λ (x : α), f x) = s₂.sum (λ (x : α), f x) - s₁.sum (λ (x : α), f x)
@[simp]
theorem finset.sum_erase_eq_sub {β : Type u} {α : Type v} {s : finset α} {f : α β} [add_comm_group β] [decidable_eq α] {a : α} (h : a s) :
(s.erase a).sum (λ (x : α), f x) = s.sum (λ (x : α), f x) - f a
@[simp]
theorem finset.prod_erase_eq_div {β : Type u} {α : Type v} {s : finset α} {f : α β} [comm_group β] [decidable_eq α] {a : α} (h : a s) :
(s.erase a).prod (λ (x : α), f x) = s.prod (λ (x : α), f x) / f a
@[simp]
theorem finset.card_sigma {α : Type v} {σ : α Type u_1} (s : finset α) (t : Π (a : α), finset (σ a)) :
(s.sigma t).card = s.sum (λ (a : α), (t a).card)
@[simp]
theorem finset.card_disj_Union {β : Type u} {α : Type v} (s : finset α) (t : α finset β) (h : s.pairwise_disjoint t) :
(s.disj_Union t h).card = s.sum (λ (i : α), (t i).card)
theorem finset.card_bUnion {β : Type u} {α : Type v} [decidable_eq β] {s : finset α} {t : α finset β} (h : (x : α), x s (y : α), y s x y disjoint (t x) (t y)) :
(s.bUnion t).card = s.sum (λ (u : α), (t u).card)
theorem finset.card_bUnion_le {β : Type u} {α : Type v} [decidable_eq β] {s : finset α} {t : α finset β} :
(s.bUnion t).card s.sum (λ (a : α), (t a).card)
theorem finset.card_eq_sum_card_fiberwise {β : Type u} {α : Type v} [decidable_eq β] {f : α β} {s : finset α} {t : finset β} (H : (x : α), x s f x t) :
s.card = t.sum (λ (a : β), (finset.filter (λ (x : α), f x = a) s).card)
theorem finset.card_eq_sum_card_image {β : Type u} {α : Type v} [decidable_eq β] (f : α β) (s : finset α) :
s.card = (finset.image f s).sum (λ (a : β), (finset.filter (λ (x : α), f x = a) s).card)
theorem finset.mem_sum {β : Type u} {α : Type v} {f : α multiset β} (s : finset α) (b : β) :
b s.sum (λ (x : α), f x) (a : α) (H : a s), b f a
theorem finset.prod_eq_zero {β : Type u} {α : Type v} {s : finset α} {a : α} {f : α β} [comm_monoid_with_zero β] (ha : a s) (h : f a = 0) :
s.prod (λ (x : α), f x) = 0
theorem finset.prod_boole {β : Type u} {α : Type v} [comm_monoid_with_zero β] {s : finset α} {p : α Prop} [decidable_pred p] :
s.prod (λ (i : α), ite (p i) 1 0) = ite ( (i : α), i s p i) 1 0
theorem finset.prod_eq_zero_iff {β : Type u} {α : Type v} {s : finset α} {f : α β} [comm_monoid_with_zero β] [nontrivial β] [no_zero_divisors β] :
s.prod (λ (x : α), f x) = 0 (a : α) (H : a s), f a = 0
theorem finset.prod_ne_zero_iff {β : Type u} {α : Type v} {s : finset α} {f : α β} [comm_monoid_with_zero β] [nontrivial β] [no_zero_divisors β] :
s.prod (λ (x : α), f x) 0 (a : α), a s f a 0
theorem finset.prod_unique_nonempty {α : Type u_1} {β : Type u_2} [comm_monoid β] [unique α] (s : finset α) (f : α β) (h : s.nonempty) :
s.prod (λ (x : α), f x) = f inhabited.default
theorem finset.sum_unique_nonempty {α : Type u_1} {β : Type u_2} [add_comm_monoid β] [unique α] (s : finset α) (f : α β) (h : s.nonempty) :
s.sum (λ (x : α), f x) = f inhabited.default
theorem finset.sum_nat_mod {α : Type v} (s : finset α) (n : ) (f : α ) :
s.sum (λ (i : α), f i) % n = s.sum (λ (i : α), f i % n) % n
theorem finset.prod_nat_mod {α : Type v} (s : finset α) (n : ) (f : α ) :
s.prod (λ (i : α), f i) % n = s.prod (λ (i : α), f i % n) % n
theorem finset.sum_int_mod {α : Type v} (s : finset α) (n : ) (f : α ) :
s.sum (λ (i : α), f i) % n = s.sum (λ (i : α), f i % n) % n
theorem finset.prod_int_mod {α : Type v} (s : finset α) (n : ) (f : α ) :
s.prod (λ (i : α), f i) % n = s.prod (λ (i : α), f i % n) % n
theorem fintype.sum_bijective {α : Type u_1} {β : Type u_2} {M : Type u_3} [fintype α] [fintype β] [add_comm_monoid M] (e : α β) (he : function.bijective e) (f : α M) (g : β M) (h : (x : α), f x = g (e x)) :
finset.univ.sum (λ (x : α), f x) = finset.univ.sum (λ (x : β), g x)

fintype.sum_equiv is a variant of finset.sum_bij that accepts function.bijective.

See function.bijective.sum_comp for a version without h.

theorem fintype.prod_bijective {α : Type u_1} {β : Type u_2} {M : Type u_3} [fintype α] [fintype β] [comm_monoid M] (e : α β) (he : function.bijective e) (f : α M) (g : β M) (h : (x : α), f x = g (e x)) :
finset.univ.prod (λ (x : α), f x) = finset.univ.prod (λ (x : β), g x)

fintype.prod_bijective is a variant of finset.prod_bij that accepts function.bijective.

See function.bijective.prod_comp for a version without h.

theorem fintype.prod_equiv {α : Type u_1} {β : Type u_2} {M : Type u_3} [fintype α] [fintype β] [comm_monoid M] (e : α β) (f : α M) (g : β M) (h : (x : α), f x = g (e x)) :
finset.univ.prod (λ (x : α), f x) = finset.univ.prod (λ (x : β), g x)

fintype.prod_equiv is a specialization of finset.prod_bij that automatically fills in most arguments.

See equiv.prod_comp for a version without h.

theorem fintype.sum_equiv {α : Type u_1} {β : Type u_2} {M : Type u_3} [fintype α] [fintype β] [add_comm_monoid M] (e : α β) (f : α M) (g : β M) (h : (x : α), f x = g (e x)) :
finset.univ.sum (λ (x : α), f x) = finset.univ.sum (λ (x : β), g x)

fintype.sum_equiv is a specialization of finset.sum_bij that automatically fills in most arguments.

See equiv.sum_comp for a version without h.

theorem fintype.sum_unique {α : Type u_1} {β : Type u_2} [add_comm_monoid β] [unique α] [fintype α] (f : α β) :
finset.univ.sum (λ (x : α), f x) = f inhabited.default
theorem fintype.prod_unique {α : Type u_1} {β : Type u_2} [comm_monoid β] [unique α] [fintype α] (f : α β) :
finset.univ.prod (λ (x : α), f x) = f inhabited.default
theorem fintype.prod_empty {α : Type u_1} {β : Type u_2} [comm_monoid β] [is_empty α] [fintype α] (f : α β) :
finset.univ.prod (λ (x : α), f x) = 1
theorem fintype.sum_empty {α : Type u_1} {β : Type u_2} [add_comm_monoid β] [is_empty α] [fintype α] (f : α β) :
finset.univ.sum (λ (x : α), f x) = 0
theorem fintype.prod_subsingleton {α : Type u_1} {β : Type u_2} [comm_monoid β] [subsingleton α] [fintype α] (f : α β) (a : α) :
finset.univ.prod (λ (x : α), f x) = f a
theorem fintype.sum_subsingleton {α : Type u_1} {β : Type u_2} [add_comm_monoid β] [subsingleton α] [fintype α] (f : α β) (a : α) :
finset.univ.sum (λ (x : α), f x) = f a
theorem fintype.prod_subtype_mul_prod_subtype {α : Type u_1} {β : Type u_2} [fintype α] [comm_monoid β] (p : α Prop) (f : α β) [decidable_pred p] :
finset.univ.prod (λ (i : {x // p x}), f i) * finset.univ.prod (λ (i : {x // ¬p x}), f i) = finset.univ.prod (λ (i : α), f i)
theorem fintype.sum_subtype_add_sum_subtype {α : Type u_1} {β : Type u_2} [fintype α] [add_comm_monoid β] (p : α Prop) (f : α β) [decidable_pred p] :
finset.univ.sum (λ (i : {x // p x}), f i) + finset.univ.sum (λ (i : {x // ¬p x}), f i) = finset.univ.sum (λ (i : α), f i)
theorem list.sum_to_finset {α : Type v} {M : Type u_1} [decidable_eq α] [add_comm_monoid M] (f : α M) {l : list α} (hl : l.nodup) :
theorem list.prod_to_finset {α : Type v} {M : Type u_1} [decidable_eq α] [comm_monoid M] (f : α M) {l : list α} (hl : l.nodup) :
theorem multiset.disjoint_list_sum_left {α : Type v} {a : multiset α} {l : list (multiset α)} :
l.sum.disjoint a (b : multiset α), b l b.disjoint a
theorem multiset.disjoint_list_sum_right {α : Type v} {a : multiset α} {l : list (multiset α)} :
a.disjoint l.sum (b : multiset α), b l a.disjoint b
theorem multiset.disjoint_sum_left {α : Type v} {a : multiset α} {i : multiset (multiset α)} :
i.sum.disjoint a (b : multiset α), b i b.disjoint a
theorem multiset.disjoint_sum_right {α : Type v} {a : multiset α} {i : multiset (multiset α)} :
a.disjoint i.sum (b : multiset α), b i a.disjoint b
theorem multiset.disjoint_finset_sum_left {α : Type v} {β : Type u_1} {i : finset β} {f : β multiset α} {a : multiset α} :
(i.sum f).disjoint a (b : β), b i (f b).disjoint a
theorem multiset.disjoint_finset_sum_right {α : Type v} {β : Type u_1} {i : finset β} {f : β multiset α} {a : multiset α} :
a.disjoint (i.sum f) (b : β), b i a.disjoint (f b)
theorem multiset.add_eq_union_left_of_le {α : Type v} [decidable_eq α] {x y z : multiset α} (h : y x) :
z + x = z y z.disjoint x x = y
theorem multiset.add_eq_union_right_of_le {α : Type v} [decidable_eq α] {x y z : multiset α} (h : z y) :
x + y = x z y = z x.disjoint y
theorem multiset.finset_sum_eq_sup_iff_disjoint {α : Type v} [decidable_eq α] {β : Type u_1} {i : finset β} {f : β multiset α} :
i.sum f = i.sup f (x : β), x i (y : β), y i x y (f x).disjoint (f y)
@[simp]
theorem multiset.to_finset_sum_count_eq {α : Type v} [decidable_eq α] (s : multiset α) :
theorem multiset.count_sum' {β : Type u} {α : Type v} [decidable_eq α] {s : finset β} {a : α} {f : β multiset α} :
multiset.count a (s.sum (λ (x : β), f x)) = s.sum (λ (x : β), multiset.count a (f x))
@[simp]
theorem multiset.to_finset_sum_count_nsmul_eq {α : Type v} [decidable_eq α] (s : multiset α) :
s.to_finset.sum (λ (a : α), multiset.count a s {a}) = s
theorem multiset.exists_smul_of_dvd_count {α : Type v} [decidable_eq α] (s : multiset α) {k : } (h : (a : α), a s k multiset.count a s) :
(u : multiset α), s = k u
theorem multiset.sum_sum {α : Type u_1} {ι : Type u_2} [add_comm_monoid α] (f : ι multiset α) (s : finset ι) :
(s.sum (λ (x : ι), f x)).sum = s.sum (λ (x : ι), (f x).sum)
theorem multiset.prod_sum {α : Type u_1} {ι : Type u_2} [comm_monoid α] (f : ι multiset α) (s : finset ι) :
(s.sum (λ (x : ι), f x)).prod = s.prod (λ (x : ι), (f x).prod)
@[simp, norm_cast]
theorem nat.cast_list_sum {β : Type u} [add_monoid_with_one β] (s : list ) :
@[simp, norm_cast]
theorem nat.cast_list_prod {β : Type u} [semiring β] (s : list ) :
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
theorem nat.cast_sum {β : Type u} {α : Type v} [add_comm_monoid_with_one β] (s : finset α) (f : α ) :
(s.sum (λ (x : α), f x)) = s.sum (λ (x : α), (f x))
@[simp, norm_cast]
theorem nat.cast_prod {β : Type u} {α : Type v} [comm_semiring β] (f : α ) (s : finset α) :
(s.prod (λ (i : α), f i)) = s.prod (λ (i : α), (f i))
@[simp, norm_cast]
theorem int.cast_list_sum {β : Type u} [add_group_with_one β] (s : list ) :
@[simp, norm_cast]
theorem int.cast_list_prod {β : Type u} [ring β] (s : list ) :
@[simp, norm_cast]
@[simp, norm_cast]
theorem int.cast_multiset_prod {R : Type u_1} [comm_ring R] (s : multiset ) :
@[simp, norm_cast]
theorem int.cast_sum {β : Type u} {α : Type v} [add_comm_group_with_one β] (s : finset α) (f : α ) :
(s.sum (λ (x : α), f x)) = s.sum (λ (x : α), (f x))
@[simp, norm_cast]
theorem int.cast_prod {α : Type v} {R : Type u_1} [comm_ring R] (f : α ) (s : finset α) :
(s.prod (λ (i : α), f i)) = s.prod (λ (i : α), (f i))
@[simp, norm_cast]
theorem units.coe_prod {α : Type v} {M : Type u_1} [comm_monoid M] (f : α Mˣ) (s : finset α) :
(s.prod (λ (i : α), f i)) = s.prod (λ (i : α), (f i))
theorem units.mk0_prod {β : Type u} {α : Type v} [comm_group_with_zero β] (s : finset α) (f : α β) (h : s.prod (λ (b : α), f b) 0) :
units.mk0 (s.prod (λ (b : α), f b)) h = s.attach.prod (λ (b : {x // x s}), units.mk0 (f b) _)
theorem nat_abs_sum_le {ι : Type u_1} (s : finset ι) (f : ι ) :
(s.sum (λ (i : ι), f i)).nat_abs s.sum (λ (i : ι), (f i).nat_abs)

additive, multiplicative #

@[simp]
@[simp]
theorem of_mul_prod {ι : Type u_1} {α : Type v} [comm_monoid α] (s : finset ι) (f : ι α) :
additive.of_mul (s.prod (λ (i : ι), f i)) = s.sum (λ (i : ι), additive.of_mul (f i))
@[simp]
theorem to_mul_sum {ι : Type u_1} {α : Type v} [comm_monoid α] (s : finset ι) (f : ι additive α) :
additive.to_mul (s.sum (λ (i : ι), f i)) = s.prod (λ (i : ι), additive.to_mul (f i))
@[simp]
theorem of_add_sum {ι : Type u_1} {α : Type v} [add_comm_monoid α] (s : finset ι) (f : ι α) :
multiplicative.of_add (s.sum (λ (i : ι), f i)) = s.prod (λ (i : ι), multiplicative.of_add (f i))
@[simp]
theorem to_add_prod {ι : Type u_1} {α : Type v} [add_comm_monoid α] (s : finset ι) (f : ι multiplicative α) :
multiplicative.to_add (s.prod (λ (i : ι), f i)) = s.sum (λ (i : ι), multiplicative.to_add (f i))