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)