# mathlibdocumentation

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.

• `∏ 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
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 α] :
finset.univ.prod (λ (i : α), f i) = 1
theorem finset.sum_of_empty {β : Type u} {α : Type v} {f : α → β} [is_empty α] :
finset.univ.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 sf 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 sf 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 sg x = g yx = 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 sg x = g yx = 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 : ∀ (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 : α → β} [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 α] [decidable_eq α] {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 α] [decidable_eq α] [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_sum_elim {β : Type u} {α : Type v} {γ : Type w} [decidable_eq γ)] (s : finset α) (t : finset γ) (f : α → β) (g : γ → β) :
(λ (x : α γ), 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 : γ → β) :
(λ (x : α γ), g x) = s.prod (λ (x : α), f x) * t.prod (λ (x : γ), g x)
@[simp]
theorem finset.sum_on_sum {β : Type u} {α : Type v} {γ : Type w} [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 : γ → } (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.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 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} [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)) :
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 sf (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 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} {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 : α → β} [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 sf x 1p 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 sf x 0p 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 sb af 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 sb af 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 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} {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} {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 α} {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 sp 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 sp 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 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 α) (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 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))) = 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 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 α} {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 α} {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 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} [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} [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.sum_pi_single' {ι : Type u_1} {M : Type u_2} [decidable_eq ι] (i : ι) (x : M) (s : finset ι) :
s.sum (λ (j : ι), 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 : ι), (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} {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 α} {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 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 : α → β} (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 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} (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 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} (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} (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 {β : 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.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 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} {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)) = 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)
theorem finset.sum_inter_add_sum_diff {β : Type u} {α : Type v} [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} [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} [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} [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} [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 : α → β} (R : setoid α)  :
s.sum (λ (x : α), f x) = (λ (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 α)  :
s.prod (λ (x : α), f x) = (λ (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 α) (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 : α → β} (R : setoid α) (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 : α), b x) = s.prod (λ (x : α), f x)
theorem finset.sum_update_of_not_mem {β : Type u} {α : Type v} [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α → β) (b : β) :
s.sum (λ (x : α), 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 : α), b x) = b * (s \ {i}).prod (λ (x : α), f x)
theorem finset.sum_update_of_mem {β : Type u} {α : Type v} [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α → β) (b : β) :
s.sum (λ (x : α), b x) = b + (s \ {i}).sum (λ (x : α), f x)
theorem finset.eq_of_card_le_one_of_sum_eq {β : Type u} {α : Type v} {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} [decidable_eq α] (s : finset α) (f : α → β) {a : α} (h : a s) :
f a + (s.erase a).sum (λ (x : α), f x) = s.sum (λ (x : α), f x)

Taking a sum over `s : finset α` is the same as adding the value on a single element `f a` to the sum over `s.erase a`.

See `multiset.sum_map_erase` for the `multiset` version.

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

Taking a product over `s : finset α` is the same as multiplying the value on a single element `f a` by the product of `s.erase a`.

See `multiset.prod_map_erase` for the `multiset` version.

theorem finset.sum_erase_add {β : Type u} {α : Type v} [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} [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 α] {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} {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} {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} {hp : decidable_pred p} :
s.sum (λ (x : α), ite (p x) 1 0) = s).card)
theorem commute.sum_right {β : Type u} {α : Type v} (s : finset α) (f : α → β) (b : β) (h : ∀ (i : α), i s (f i)) :
(s.sum (λ (i : α), f i))
theorem commute.sum_left {β : Type u} {α : Type v} (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} {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} {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 : α → β}  :
s.sum (λ (x : α), -f x) = -s.sum (λ (x : α), f x)
@[simp]
theorem finset.prod_inv_distrib {β : Type u} {α : Type v} {s : finset α} {f : α → β}  :
s.prod (λ (x : α), (f x)⁻¹) = (s.prod (λ (x : α), f x))⁻¹
@[simp]
theorem finset.sum_sub_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)
@[simp]
theorem finset.prod_div_distrib {β : Type u} {α : Type v} {s : finset α} {f g : α → β}  :
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} (f : α → β) (s : finset α) (n : ) :
s.sum (λ (a : α), n f a) = n s.sum (λ (a : α), f a)
theorem finset.prod_zpow {β : Type u} {α : Type v} (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 : α → β} [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 : α → β} [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 : α → β} [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 : α → } (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 : α → } :
(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 = s).sum (λ (a : β), (finset.filter (λ (x : α), f x = a) s).card)
theorem finset.mem_sum {β : Type u} {α : Type v} {f : α → } (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 : α → β} (ha : a s) (h : f a = 0) :
s.prod (λ (x : α), f x) = 0
theorem finset.prod_boole {β : Type u} {α : Type v} {s : finset α} {p : α → Prop}  :
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 : α → β} [nontrivial β]  :
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 : α → β} [nontrivial β]  :
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) =
theorem finset.sum_unique_nonempty {α : Type u_1} {β : Type u_2} [unique α] (s : finset α) (f : α → β) (h : s.nonempty) :
s.sum (λ (x : α), f x) =
theorem fintype.sum_bijective {α : Type u_1} {β : Type u_2} {M : Type u_3} [fintype α] [fintype β] (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 β] (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} [unique α] (f : α → β) :
finset.univ.sum (λ (x : α), f x) =
theorem fintype.prod_unique {α : Type u_1} {β : Type u_2} [comm_monoid β] [unique α] (f : α → β) :
finset.univ.prod (λ (x : α), f x) =
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} [is_empty α] (f : α → β) :
finset.univ.sum (λ (x : α), f x) = 0
theorem fintype.prod_subsingleton {α : Type u_1} {β : Type u_2} [comm_monoid β] [subsingleton α] [fintype α] (f : α → β) (a : α) :
finset.univ.prod (λ (x : α), f x) = f a
theorem fintype.sum_subsingleton {α : Type u_1} {β : Type u_2} [subsingleton α] [fintype α] (f : α → β) (a : α) :
finset.univ.sum (λ (x : α), f x) = f a
theorem fintype.prod_subtype_mul_prod_subtype {α : Type u_1} {β : Type u_2} [fintype α] [comm_monoid β] (p : α → Prop) (f : α → β)  :
finset.univ.prod (λ (i : {x // p x}), f i) * finset.univ.prod (λ (i : {x // ¬p x}), f i) = finset.univ.prod (λ (i : α), f i)
theorem fintype.sum_subtype_add_sum_subtype {α : Type u_1} {β : Type u_2} [fintype α] (p : α → Prop) (f : α → β)  :
finset.univ.sum (λ (i : {x // p x}), f i) + finset.univ.sum (λ (i : {x // ¬p x}), f i) = finset.univ.sum (λ (i : α), f i)
theorem list.sum_to_finset {α : Type v} {M : Type u_1} [decidable_eq α] (f : α → M) {l : list α} (hl : l.nodup) :
theorem list.prod_to_finset {α : Type v} {M : Type u_1} [decidable_eq α] [comm_monoid M] (f : α → M) {l : list α} (hl : l.nodup) :
theorem multiset.disjoint_list_sum_left {α : Type v} {a : multiset α} {l : list (multiset α)} :
l.sum.disjoint a ∀ (b : multiset α), b lb.disjoint a
theorem multiset.disjoint_list_sum_right {α : Type v} {a : multiset α} {l : list (multiset α)} :
a.disjoint l.sum ∀ (b : multiset α), b la.disjoint b
theorem multiset.disjoint_sum_left {α : Type v} {a : multiset α} {i : multiset (multiset α)} :
i.sum.disjoint a ∀ (b : multiset α), b ib.disjoint a
theorem multiset.disjoint_sum_right {α : Type v} {a : multiset α} {i : multiset (multiset α)} :
a.disjoint i.sum ∀ (b : multiset α), b ia.disjoint b
theorem multiset.disjoint_finset_sum_left {α : Type v} {β : Type u_1} {i : finset β} {f : β → } {a : multiset α} :
(i.sum f).disjoint a ∀ (b : β), b i(f b).disjoint a