mathlib documentation

algebra.big_operators.basic

Big operators #

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

Notation #

We introduce the following notation, localized in 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
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]
theorem ring_hom.unop_map_list_prod {β : Type u} {γ : Type w} [semiring β] [semiring γ] (f : β →+* γᵐᵒᵖ) (l : list β) :

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 α] :
finset.univ.prod (λ (i : α), f i) = 1
theorem finset.sum_of_empty {β : Type u} {α : Type v} {f : α → β} [add_comm_monoid β] [is_empty α] :
finset.univ.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 sf 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 sf 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 sg x = g yx = 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 sg x = g yx = 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 : ∀ (a : α), a s₁a 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 : ∀ (a : α), a s₁a s₂) :
(s₁.disj_union s₂ h).prod (λ (x : α), f x) = s₁.prod (λ (x : α), f x) * s₂.prod (λ (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 α] [decidable_eq α] [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 α] [decidable_eq α] [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_sum_elim {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] [decidable_eq γ)] (s : finset α) (t : finset γ) (f : α → β) (g : γ → β) :
(finset.map function.embedding.inl s finset.map function.embedding.inr t).sum (λ (x : α γ), sum.elim f g x) = s.sum (λ (x : α), f x) + t.sum (λ (x : γ), g x)
@[simp]
theorem finset.prod_sum_elim {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] [decidable_eq γ)] (s : finset α) (t : finset γ) (f : α → β) (g : γ → β) :
(finset.map function.embedding.inl s finset.map function.embedding.inr t).prod (λ (x : α γ), sum.elim f g x) = s.prod (λ (x : α), f x) * t.prod (λ (x : γ), g x)
@[simp]
theorem finset.sum_on_sum {β : Type u} {α : Type v} {γ : Type w} [add_comm_monoid β] [fintype α] [fintype γ] (f : α γ → β) :
finset.univ.sum (λ (x : α γ), f x) = finset.univ.sum (λ (x : α), f (sum.inl x)) + finset.univ.sum (λ (x : γ), f (sum.inr x))
@[simp]
theorem finset.prod_on_sum {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] [fintype α] [fintype γ] (f : α γ → β) :
finset.univ.prod (λ (x : α γ), f x) = finset.univ.prod (λ (x : α), f (sum.inl x)) * finset.univ.prod (λ (x : γ), f (sum.inr 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.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 sg 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 sg 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 sf (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 sf (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.product 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.product 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.product 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.product 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.product 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.product 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.product 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.product 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 cr (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 cr (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 sf 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 sf 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 sf x 1p 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 sf x 0p 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 sb af 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 sb af 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 sb af b = 0) (h₁ : a sf 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 sb af b = 1) (h₁ : a sf 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 sc a c bf 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 sc a c bf 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 sc a c bf c = 1) (ha : a sf a = 1) (hb : b sf 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 sc a c bf c = 0) (ha : a sf a = 0) (hb : b sf 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 sp 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 sp 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 sg 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 sg 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 sf 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 sf 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 sp 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 sp 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 sp 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 sp 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.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.sum_pi_single' {ι : Type u_1} {M : Type u_2} [decidable_eq ι] [add_comm_monoid M] (i : ι) (x : M) (s : finset ι) :
s.sum (λ (j : ι), pi.single i x j) = ite (i s) x 0
@[simp]
theorem finset.sum_pi_single {ι : Type u_1} {M : ι → Type u_2} [decidable_eq ι] [Π (i : ι), add_comm_monoid (M i)] (i : ι) (f : Π (i : ι), M i) (s : finset ι) :
s.sum (λ (j : ι), pi.single j (f j) i) = ite (i s) (f i) 0
theorem finset.prod_bij_ne_one {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] {s : finset α} {t : finset γ} {f : α → β} {g : γ → β} (i : Π (a : α), a sf a 1 → γ) (hi : ∀ (a : α) (h₁ : a s) (h₂ : f a 1), i a h₁ h₂ t) (i_inj : ∀ (a₁ a₂ : α) (h₁₁ : a₁ s) (h₁₂ : f a₁ 1) (h₂₁ : a₂ s) (h₂₂ : f a₂ 1), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂a₁ = a₂) (i_surj : ∀ (b : γ), b tg b 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 sf a 0 → γ) (hi : ∀ (a : α) (h₁ : a s) (h₂ : f a 0), i a h₁ h₂ t) (i_inj : ∀ (a₁ a₂ : α) (h₁₁ : a₁ s) (h₁₂ : f a₁ 0) (h₂₁ : a₂ s) (h₂₂ : f a₂ 0), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂a₁ = a₂) (i_surj : ∀ (b : γ), b tg b 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 sp 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 sp 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 Nu 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 Nu 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.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 ap bp (a * b)) (p_one : p 1) (p_s : ∀ (x : α), x sp (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 ap bp (a + b)) (p_one : p 0) (p_s : ∀ (x : α), x sp (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 ap bp (a + b)) (hs_nonempty : s.nonempty) (p_s : ∀ (x : α), x sp (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 ap bp (a * b)) (hs_nonempty : s.nonempty) (p_s : ∀ (x : α), x sp (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 {M : Type u_1} [comm_monoid M] (f s : → M) (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 {M : Type u_1} [add_comm_monoid M] (f s : → M) (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 {G : Type u_1} [add_comm_group G] (f : → G) (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.sum_range_sub' {G : Type u_1} [add_comm_group G] (f : → G) (n : ) :
(finset.range n).sum (λ (i : ), f i - f (i + 1)) = f 0 - f n
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_of_monotone {α : 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.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 1g 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 0g 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.

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.

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.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.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 sx af 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 sx af 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 Sg1 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 sj ig j = f j) (h3 : ∀ (j : α), j sj ih 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 sf 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 finset.eq_sum_range_sub {β : Type u} [add_comm_group β] (f : → β) (n : ) :
f n = f 0 + (finset.range n).sum (λ (i : ), f (i + 1) - f i)
theorem finset.eq_sum_range_sub' {β : Type u} [add_comm_group β] (f : → β) (n : ) :
f n = (finset.range (n + 1)).sum (λ (i : ), ite (i = 0) (f 0) (f i - f (i - 1)))
theorem commute.sum_right {β : Type u} {α : Type v} [non_unital_non_assoc_semiring β] (s : finset α) (f : α → β) (b : β) (h : ∀ (i : α), i scommute 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 scommute (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)
theorem finset.card_bUnion {β : Type u} {α : Type v} [decidable_eq β] {s : finset α} {t : α → finset β} (h : ∀ (x : α), x s∀ (y : α), y sx ydisjoint (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 sf 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 sp 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 sf 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 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 α] (f : α → β) :
finset.univ.sum (λ (x : α), f x) = f inhabited.default
theorem fintype.prod_unique {α : Type u_1} {β : Type u_2} [comm_monoid β] [unique α] (f : α → β) :
finset.univ.prod (λ (x : α), f x) = f inhabited.default
theorem fintype.prod_empty {α : Type u_1} {β : Type u_2} [comm_monoid β] [is_empty α] (f : α → β) :
finset.univ.prod (λ (x : α), f x) = 1
theorem fintype.sum_empty {α : Type u_1} {β : Type u_2} [add_comm_monoid β] [is_empty α] (f : α → β) :
finset.univ.sum (λ (x : α), f x) = 0
theorem fintype.prod_subsingleton {α : Type u_1} {β : Type u_2} [comm_monoid β] [subsingleton α] (f : α → β) (a : α) :
finset.univ.prod (λ (x : α), f x) = f a
theorem fintype.sum_subsingleton {α : Type u_1} {β : Type u_2} [add_comm_monoid β] [subsingleton α] (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) =