# mathlib3documentation

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.

• `∏ x in s, f x` is notation for `finset.prod s f` (assuming `β` is a `comm_monoid`)
• `∑ x in s, f x` is notation for `finset.sum s f` (assuming `β` is an `add_comm_monoid`)
• `∏ x, f x` is notation for `finset.prod finset.univ f` (assuming `α` is a `fintype` and `β` is a `comm_monoid`)
• `∑ x, f x` is notation for `finset.sum finset.univ f` (assuming `α` is a `fintype` and `β` is an `add_comm_monoid`)

## 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} (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 = s).prod
@[simp]
theorem finset.sum_mk {β : Type u} {α : Type v} (s : multiset α) (hs : s.nodup) (f : α β) :
{val := s, nodup := hs}.sum f = s).sum
@[simp]
theorem finset.sum_val {α : Type v} (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) = s.val).prod
theorem finset.sum_eq_multiset_sum {β : Type u} {α : Type v} (s : finset α) (f : α β) :
s.sum (λ (x : α), f x) = s.val).sum
@[simp]
theorem finset.prod_map_val {β : Type u} {α : Type v} [comm_monoid β] (s : finset α) (f : α β) :
s.val).prod = s.prod (λ (a : α), f a)
@[simp]
theorem finset.sum_map_val {β : Type u} {α : Type v} (s : finset α) (f : α β) :
s.val).sum = s.sum (λ (a : α), f a)
theorem finset.prod_eq_fold {β : Type u} {α : Type v} [comm_monoid β] (s : finset α) (f : α β) :
s.prod (λ (x : α), f x) = s
theorem finset.sum_eq_fold {β : Type u} {α : Type v} (s : finset α) (f : α β) :
s.sum (λ (x : α), f x) = 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} {G : Type u_1} [ γ] (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} [ γ] (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} (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} (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 β) :
f l.prod = l).prod

Deprecated: use `_root_.map_list_prod` instead.

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

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} (f : β →+* γ) (s : multiset β) :
f s.prod = s).prod

Deprecated: use `_root_.map_multiset_prod` instead.

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

Deprecated: use `_root_.map_multiset_sum` instead.

@[protected]
theorem ring_hom.map_prod {β : Type u} {α : Type v} {γ : Type w} (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} (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} (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} [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} (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} [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 : α β}  :
.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 : α β} [is_empty α] (s : finset α) :
s.sum (λ (i : α), f i) = 0
@[simp]
theorem finset.sum_cons {β : Type u} {α : Type v} {s : finset α} {a : α} {f : α β} (h : a s) :
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) :
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 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 : α β} [decidable_eq α] :
a s 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 : α β} [decidable_eq α] (h : a s f a = 0) :
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) :
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 : α β} [decidable_eq α] (h : f a = 0) :
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) :
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 : α β}  :
{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 : α β} [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 α}  :
s.sum (λ (x : α), 0) = 0
@[simp]
theorem finset.sum_image {β : Type u} {α : Type v} {γ : Type w} {f : α β} [decidable_eq α] {s : finset γ} {g : γ α} :
( (x : γ), x s (y : γ), y s g x = g y x = y) 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) s).prod (λ (x : α), f x) = s.prod (λ (x : γ), f (g x))
@[simp]
theorem finset.sum_map {β : Type u} {α : Type v} {γ : Type w} (s : finset α) (e : α γ) (f : γ β) :
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 : γ β) :
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 : α β} (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 : α β} (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 : ι ) (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 : α β} (s : finset ι) (t : ι ) (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 : α β} [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 : α β} [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} (s : finset α) (p : α Prop) [decidable_pred (λ (x : α), ¬p x)] (f : α β) :
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 (λ (x : α), ¬p x)] (f : α β) :
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} (s : finset α) (f : α β) :
theorem equiv.perm.sum_comp {β : Type u} {α : Type v} (σ : 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} (σ : 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 α] {s t : finset α} (h : 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 : 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} [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} [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 : α β} [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} (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} (s : finset α) (t : finset γ) (f : α β) (g : γ β) :
(s.disj_sum t).sum (λ (x : α γ), 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 : α γ), 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 : γ } (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 : α β} [decidable_eq α] {s : finset γ} {t : γ } (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 : β) :
(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} {σ : α Type u_1} (s : finset α) (t : Π (a : α), finset (σ a)) (f : β) :
(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} {σ : α 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} {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} {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 = 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} {ι' : Type u_2} [decidable_eq ι] (e : ι ι') (f : ι' β) {s' : finset ι'} {s : finset ι} (h : s = 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} (r : finset × α)) (s : finset γ) (t : γ ) (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 : γ ) (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} (r : finset × α)) (s : finset γ) (t : γ ) (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 : γ ) (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 : γ ) (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} (r : finset × γ)) (s : finset γ) (t : γ ) (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 : γ ) (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} (r : finset × γ)) (s : finset γ) (t : γ ) (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} [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)) :
s).prod (λ (x : α), f x) = s.prod (λ (x : γ), h x)
theorem finset.sum_image' {β : Type u} {α : Type v} {γ : Type w} {f : α β} [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)) :
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 : α β}  :
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} {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} {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} {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} {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} {s : finset γ} {t : γ } {t' : finset α} {s' : α } (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 `finset`s depend on the outer variable.

theorem finset.prod_comm' {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] {s : finset γ} {t : γ } {t' : finset α} {s' : α } (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 `finset`s 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} {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} {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} {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 : α β} [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 : α β} (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} (hp : (x : α), x s f x 1 p x) :
s).prod (λ (x : α), f x) = s.prod (λ (x : α), f x)
theorem finset.sum_filter_of_ne {β : Type u} {α : Type v} {s : finset α} {f : α β} {p : α Prop} (hp : (x : α), x s f x 0 p x) :
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 : α β} [Π (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) (f : α β) :
s).prod (λ (a : α), f a) = s.prod (λ (a : α), ite (p a) (f a) 1)
theorem finset.sum_filter {β : Type u} {α : Type v} {s : finset α} (p : α Prop) (f : α β) :
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} {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} {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} {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} {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 α} {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}  :
s).prod (λ (x : subtype p), f x) = 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 α} (f : α β) {p : α Prop}  :
s).sum (λ (x : subtype p), f x) = 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} (h : (x : α), x s p x) :
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 α} (f : α β) {p : α Prop} (h : (x : α), x s p x) :
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} {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 α) (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 : α β)  :
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} (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} {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} {β : 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))) = s).attach.prod (λ (x : {x // x 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} {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))) = s).attach.sum (λ (x : {x // x 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))) = 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} {s : finset α} {p : α Prop} {hp : decidable_pred p} (f g : α γ) (h : γ β) :
s.sum (λ (x : α), h (ite (p x) (f x) (g x))) = 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} {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)) = s).attach.sum (λ (x : {x // x 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)) = s).attach.prod (λ (x : {x // x 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)) = s).prod (λ (x : α), f x) * (finset.filter (λ (x : α), ¬p x) s).prod (λ (x : α), g x)
theorem finset.sum_ite {β : Type u} {α : Type v} {s : finset α} {p : α Prop} {hp : decidable_pred p} (f g : α β) :
s.sum (λ (x : α), ite (p x) (f x) (g x)) = 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 α} {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 α} {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 α} {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 α} {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} [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} [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} [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} [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} [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} [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} (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} (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} (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' : α), a') = ite (a s) x 1
@[simp]
theorem finset.sum_pi_single' {β : Type u} {α : Type v} [decidable_eq α] (a : α) (x : β) (s : finset α) :
s.sum (λ (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' : α), (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' : α), (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} {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 α} {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 α} {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 : α β} (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 : α β} (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} (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} (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} (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} {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} (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} (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} (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} (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} (f : α M) :
(list.map f l).sum = l.to_finset.sum (λ (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 ^ l)
theorem finset.sum_list_count {α : Type v} [decidable_eq α] (s : list α) :
s.sum = s.to_finset.sum (λ (m : α), s m)
theorem finset.prod_list_count {α : Type v} [decidable_eq α] [comm_monoid α] (s : list α) :
s.prod = s.to_finset.prod (λ (m : α), 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 ^ m)
theorem finset.sum_list_count_of_subset {α : Type v} [decidable_eq α] (m : list α) (s : finset α) (hs : m.to_finset s) :
m.sum = s.sum (λ (i : α), m i)
theorem finset.sum_filter_count_eq_countp {α : Type v} [decidable_eq α] (p : α Prop) (l : list α) :
l.to_finset).sum (λ (x : α), l) = l
theorem finset.prod_multiset_map_count {α : Type v} [decidable_eq α] (s : multiset α) {M : Type u_1} [comm_monoid M] (f : α M) :
s).prod = s.to_finset.prod (λ (m : α), f m ^ s)
theorem finset.sum_multiset_map_count {α : Type v} [decidable_eq α] (s : multiset α) {M : Type u_1} (f : α M) :
s).sum = s.to_finset.sum (λ (m : α), f m)
theorem finset.sum_multiset_count {α : Type v} [decidable_eq α] (s : multiset α) :
s.sum = s.to_finset.sum (λ (m : α), m)
theorem finset.prod_multiset_count {α : Type v} [decidable_eq α] [comm_monoid α] (s : multiset α) :
s.prod = s.to_finset.prod (λ (m : α), 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 ^ m)
theorem finset.sum_multiset_count_of_subset {α : Type v} [decidable_eq α] (m : multiset α) (s : finset α) (hs : m.to_finset s) :
m.sum = s.sum (λ (i : α), i)
theorem finset.sum_mem_multiset {β : Type u} {α : Type v} [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} (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} (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} (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} (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} (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} (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} (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} [has_sub α] {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 α} (b : β) :
s.sum (λ (x : α), b) = s.card b
theorem finset.sum_eq_card_nsmul {β : Type u} {α : Type v} {s : finset α} {f : α β} {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} (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} (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} {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} {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)) = 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 α} [decidable_eq γ] (f : γ β) (g : α γ) :
s.sum (λ (a : α), f (g a)) = 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} [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)