# 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.

def finset.sum {β : Type u} {α : Type v} (s : finset α) (f : α → β) :
β

`∑ x in s, f` is the sum of `f x` as `x` ranges over the elements of the finite set `s`.

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
theorem finset.prod_eq_multiset_prod {β : Type u} {α : Type v} [comm_monoid β] (s : finset α) (f : α → β) :
∏ (x : α) in s, f x = s.val).prod
theorem finset.sum_eq_multiset_sum {β : Type u} {α : Type v} (s : finset α) (f : α → β) :
∑ (x : α) in s, f x = s.val).sum
theorem finset.prod_eq_fold {β : Type u} {α : Type v} [comm_monoid β] (s : finset α) (f : α → β) :
∏ (x : α) in s, f x = s
theorem finset.sum_eq_fold {β : Type u} {α : Type v} (s : finset α) (f : α → β) :
∑ (x : α) in s, f x = s
@[simp]
theorem finset.sum_multiset_singleton {α : Type v} (s : finset α) :
∑ (x : α) in s, (x ::ₘ 0) = s.val
theorem add_monoid_hom.map_sum {β : Type u} {α : Type v} {γ : Type w} (g : β →+ γ) (f : α → β) (s : finset α) :
g (∑ (x : α) in s, f x) = ∑ (x : α) in s, g (f x)
theorem monoid_hom.map_prod {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] [comm_monoid γ] (g : β →* γ) (f : α → β) (s : finset α) :
g (∏ (x : α) in s, f x) = ∏ (x : α) in s, g (f x)
theorem add_equiv.map_sum {β : Type u} {α : Type v} {γ : Type w} (g : β ≃+ γ) (f : α → β) (s : finset α) :
g (∑ (x : α) in s, f x) = ∑ (x : α) in s, g (f x)
theorem mul_equiv.map_prod {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] [comm_monoid γ] (g : β ≃* γ) (f : α → β) (s : finset α) :
g (∏ (x : α) in s, f x) = ∏ (x : α) in s, g (f x)
theorem ring_hom.map_list_prod {β : Type u} {γ : Type w} [semiring β] [semiring γ] (f : β →+* γ) (l : list β) :
f l.prod = l).prod
theorem ring_hom.map_list_sum {β : Type u} {γ : Type w} (f : β →+* γ) (l : list β) :
f l.sum = l).sum
theorem ring_hom.map_multiset_prod {β : Type u} {γ : Type w} (f : β →+* γ) (s : multiset β) :
f s.prod = s).prod
theorem ring_hom.map_multiset_sum {β : Type u} {γ : Type w} (f : β →+* γ) (s : multiset β) :
f s.sum = s).sum
theorem ring_hom.map_prod {β : Type u} {α : Type v} {γ : Type w} (g : β →+* γ) (f : α → β) (s : finset α) :
g (∏ (x : α) in s, f x) = ∏ (x : α) in s, g (f x)
theorem ring_hom.map_sum {β : Type u} {α : Type v} {γ : Type w} (g : β →+* γ) (f : α → β) (s : finset α) :
g (∑ (x : α) in s, f x) = ∑ (x : α) in s, g (f x)
theorem add_monoid_hom.coe_sum {β : Type u} {α : Type v} {γ : Type w} (f : α → β →+ γ) (s : finset α) :
∑ (x : α) in s, f x = ∑ (x : α) in s, (f x)
theorem monoid_hom.coe_prod {β : Type u} {α : Type v} {γ : Type w} [comm_monoid γ] (f : α → β →* γ) (s : finset α) :
∏ (x : α) in s, f x = ∏ (x : α) in s, (f x)
@[simp]
theorem add_monoid_hom.finset_sum_apply {β : Type u} {α : Type v} {γ : Type w} (f : α → β →+ γ) (s : finset α) (b : β) :
(∑ (x : α) in s, f x) b = ∑ (x : α) in s, (f x) b
@[simp]
theorem monoid_hom.finset_prod_apply {β : Type u} {α : Type v} {γ : Type w} [comm_monoid γ] (f : α → β →* γ) (s : finset α) (b : β) :
(∏ (x : α) in s, f x) b = ∏ (x : α) in s, (f x) b
@[simp]
theorem finset.sum_empty {β : Type u} {α : Type v} {f : α → β} :
∑ (x : α) in , f x = 0
@[simp]
theorem finset.prod_empty {β : Type u} {α : Type v} [comm_monoid β] {f : α → β} :
∏ (x : α) in , f x = 1
@[simp]
theorem finset.prod_insert {β : Type u} {α : Type v} {s : finset α} {a : α} {f : α → β} [comm_monoid β] [decidable_eq α] :
a s∏ (x : α) in s, f x = (f a) * ∏ (x : α) in s, f x
@[simp]
theorem finset.sum_insert {β : Type u} {α : Type v} {s : finset α} {a : α} {f : α → β} [decidable_eq α] :
a s∑ (x : α) in s, f x = f a + ∑ (x : α) in s, 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) :
∑ (x : α) in s, f x = ∑ (x : α) in s, 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) :
∏ (x : α) in s, f x = ∏ (x : α) in s, 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) :
∑ (x : α) in s, f x = ∑ (x : α) in s, 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) :
∏ (x : α) in s, f x = ∏ (x : α) in s, 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 β] :
∏ (x : α) in {a}, f x = f a
@[simp]
theorem finset.sum_singleton {β : Type u} {α : Type v} {a : α} {f : α → β}  :
∑ (x : α) in {a}, f x = f a
theorem finset.prod_pair {β : Type u} {α : Type v} {f : α → β} [comm_monoid β] [decidable_eq α] {a b : α} (h : a b) :
∏ (x : α) in {a, b}, f x = (f a) * f b
theorem finset.sum_pair {β : Type u} {α : Type v} {f : α → β} [decidable_eq α] {a b : α} (h : a b) :
∑ (x : α) in {a, b}, f x = f a + f b
@[simp]
theorem finset.prod_const_one {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] :
∏ (x : α) in s, 1 = 1
@[simp]
theorem finset.sum_const_zero {β : Type u} {α : Type v} {s : finset α}  :
∑ (x : α) in s, 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)∑ (x : α) in s, f x = ∑ (x : γ) in s, 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)∏ (x : α) in s, f x = ∏ (x : γ) in s, f (g x)
@[simp]
theorem finset.sum_map {β : Type u} {α : Type v} {γ : Type w} (s : finset α) (e : α γ) (f : γ → β) :
∑ (x : γ) in s, f x = ∑ (x : α) in s, f (e x)
@[simp]
theorem finset.prod_map {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] (s : finset α) (e : α γ) (f : γ → β) :
∏ (x : γ) in s, f x = ∏ (x : α) in s, 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_union_inter {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α → β} [decidable_eq α] :
∑ (x : α) in s₁ s₂, f x + ∑ (x : α) in s₁ s₂, f x = ∑ (x : α) in s₁, f x + ∑ (x : α) in s₂, f x
theorem finset.prod_union_inter {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α → β} [comm_monoid β] [decidable_eq α] :
(∏ (x : α) in s₁ s₂, f x) * ∏ (x : α) in s₁ s₂, f x = (∏ (x : α) in s₁, f x) * ∏ (x : α) in s₂, f x
theorem finset.prod_union {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α → β} [comm_monoid β] [decidable_eq α] (h : disjoint s₁ s₂) :
∏ (x : α) in s₁ s₂, f x = (∏ (x : α) in s₁, f x) * ∏ (x : α) in s₂, f x
theorem finset.sum_union {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α → β} [decidable_eq α] (h : disjoint s₁ s₂) :
∑ (x : α) in s₁ s₂, f x = ∑ (x : α) in s₁, f x + ∑ (x : α) in s₂, f x
theorem is_compl.sum_add_sum {β : Type u} {α : Type v} [fintype α] [decidable_eq α] {s t : finset α} (h : t) (f : α → β) :
∑ (i : α) in s, f i + ∑ (i : α) in t, f i = ∑ (i : α), f i
theorem is_compl.prod_mul_prod {β : Type u} {α : Type v} [fintype α] [decidable_eq α] [comm_monoid β] {s t : finset α} (h : t) (f : α → β) :
(∏ (i : α) in s, f i) * ∏ (i : α) in t, f i = ∏ (i : α), f i
theorem finset.sum_add_sum_compl {β : Type u} {α : Type v} [fintype α] [decidable_eq α] (s : finset α) (f : α → β) :
∑ (i : α) in s, f i + ∑ (i : α) in s, f i = ∑ (i : α), f i
theorem finset.prod_mul_prod_compl {β : Type u} {α : Type v} [comm_monoid β] [fintype α] [decidable_eq α] (s : finset α) (f : α → β) :
(∏ (i : α) in s, f i) * ∏ (i : α) in s, f i = ∏ (i : α), f i
theorem finset.prod_compl_mul_prod {β : Type u} {α : Type v} [comm_monoid β] [fintype α] [decidable_eq α] (s : finset α) (f : α → β) :
(∏ (i : α) in s, f i) * ∏ (i : α) in s, f i = ∏ (i : α), f i
theorem finset.sum_compl_add_sum {β : Type u} {α : Type v} [fintype α] [decidable_eq α] (s : finset α) (f : α → β) :
∑ (i : α) in s, f i + ∑ (i : α) in s, f i = ∑ (i : α), f i
theorem finset.prod_sdiff {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α → β} [comm_monoid β] [decidable_eq α] (h : s₁ s₂) :
(∏ (x : α) in s₂ \ s₁, f x) * ∏ (x : α) in s₁, f x = ∏ (x : α) in s₂, f x
theorem finset.sum_sdiff {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α → β} [decidable_eq α] (h : s₁ s₂) :
∑ (x : α) in s₂ \ s₁, f x + ∑ (x : α) in s₁, f x = ∑ (x : α) in s₂, f x
@[simp]
theorem finset.sum_sum_elim {β : Type u} {α : Type v} {γ : Type w} [decidable_eq γ)] (s : finset α) (t : finset γ) (f : α → β) (g : γ → β) :
∑ (x : α γ) in , g x = ∑ (x : α) in s, f x + ∑ (x : γ) in t, 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 : α γ) in , g x = (∏ (x : α) in s, f x) * ∏ (x : γ) in t, g x
theorem finset.prod_bUnion {β : Type u} {α : Type v} {γ : Type w} {f : α → β} [comm_monoid β] [decidable_eq α] {s : finset γ} {t : γ → } :
(∀ (x : γ), x s∀ (y : γ), y sx ydisjoint (t x) (t y))∏ (x : α) in s.bUnion t, f x = ∏ (x : γ) in s, ∏ (i : α) in t x, f i
theorem finset.sum_bUnion {β : Type u} {α : Type v} {γ : Type w} {f : α → β} [decidable_eq α] {s : finset γ} {t : γ → } :
(∀ (x : γ), x s∀ (y : γ), y sx ydisjoint (t x) (t y))∑ (x : α) in s.bUnion t, f x = ∑ (x : γ) in s, ∑ (i : α) in t x, f i
theorem finset.prod_product {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] {s : finset γ} {t : finset α} {f : γ × α → β} :
∏ (x : γ × α) in s.product t, f x = ∏ (x : γ) in s, ∏ (y : α) in t, f (x, y)
theorem finset.sum_product {β : Type u} {α : Type v} {γ : Type w} {s : finset γ} {t : finset α} {f : γ × α → β} :
∑ (x : γ × α) in s.product t, f x = ∑ (x : γ) in s, ∑ (y : α) in t, f (x, y)
theorem finset.sum_product' {β : Type u} {α : Type v} {γ : Type w} {s : finset γ} {t : finset α} {f : γ → α → β} :
∑ (x : γ × α) in s.product t, f x.fst x.snd = ∑ (x : γ) in s, ∑ (y : α) in t, 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 : γ → α → β} :
∏ (x : γ × α) in s.product t, f x.fst x.snd = ∏ (x : γ) in s, ∏ (y : α) in t, f x y

An uncurried version of `finset.prod_product`.

theorem finset.prod_sigma {β : Type u} {α : Type v} [comm_monoid β] {σ : α → Type u_1} (s : finset α) (t : Π (a : α), finset (σ a)) (f : → β) :
∏ (x : Σ (a : α), σ a) in s.sigma t, f x = ∏ (a : α) in s, ∏ (s : σ a) in t 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 : → β) :
∑ (x : Σ (a : α), σ a) in s.sigma t, f x = ∑ (a : α) in s, ∑ (s : σ a) in t 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 → β) :
∑ (a : α) in s, ∑ (s : σ a) in t a, f a s = ∑ (x : Σ (a : α), σ a) in s.sigma t, 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 → β) :
∏ (a : α) in s, ∏ (s : σ a) in t a, f a s = ∏ (x : Σ (a : α), σ a) in s.sigma t, f x.fst x.snd
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 : α → β) :
∏ (y : γ) in t, ∏ (x : α) in finset.filter (λ (x : α), g x = y) s, f x = ∏ (x : α) in s, 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 : α → β) :
∑ (y : γ) in t, ∑ (x : α) in finset.filter (λ (x : α), g x = y) s, f x = ∑ (x : α) in s, 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) = ∏ (x : γ) in finset.filter (λ (c' : γ), g c' = g c) s, h x) :
∏ (x : α) in s, f x = ∏ (x : γ) in s, 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) = ∑ (x : γ) in finset.filter (λ (c' : γ), g c' = g c) s, h x) :
∑ (x : α) in s, f x = ∑ (x : γ) in s, h x
theorem finset.prod_mul_distrib {β : Type u} {α : Type v} {s : finset α} {f g : α → β} [comm_monoid β] :
∏ (x : α) in s, (f x) * g x = (∏ (x : α) in s, f x) * ∏ (x : α) in s, g x
theorem finset.sum_add_distrib {β : Type u} {α : Type v} {s : finset α} {f g : α → β}  :
∑ (x : α) in s, (f x + g x) = ∑ (x : α) in s, f x + ∑ (x : α) in s, g x
theorem finset.prod_comm {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] {s : finset γ} {t : finset α} {f : γ → α → β} :
∏ (x : γ) in s, ∏ (y : α) in t, f x y = ∏ (y : α) in t, ∏ (x : γ) in s, f x y
theorem finset.sum_comm {β : Type u} {α : Type v} {γ : Type w} {s : finset γ} {t : finset α} {f : γ → α → β} :
∑ (x : γ) in s, ∑ (y : α) in t, f x y = ∑ (y : α) in t, ∑ (x : γ) in s, f x y
theorem finset.prod_hom {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] [comm_monoid γ] (s : finset α) {f : α → β} (g : β → γ)  :
∏ (x : α) in s, g (f x) = g (∏ (x : α) in s, f x)
theorem finset.sum_hom {β : Type u} {α : Type v} {γ : Type w} (s : finset α) {f : α → β} (g : β → γ)  :
∑ (x : α) in s, g (f x) = g (∑ (x : α) in s, f x)
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 (∑ (x : α) in s, f x) (∑ (x : α) in s, 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 (∏ (x : α) in s, f x) (∏ (x : α) in s, g x)
theorem finset.sum_subset {β : Type u} {α : Type v} {s₁ s₂ : finset α} {f : α → β} (h : s₁ s₂) (hf : ∀ (x : α), x s₂x s₁f x = 0) :
∑ (x : α) in s₁, f x = ∑ (x : α) in s₂, 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) :
∏ (x : α) in s₁, f x = ∏ (x : α) in s₂, 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) :
∏ (x : α) in , f x = ∏ (x : α) in s, f x
theorem finset.sum_filter_of_ne {β : Type u} {α : Type v} {s : finset α} {f : α → β} {p : α → Prop} (hp : ∀ (x : α), x sf x 0p x) :
∑ (x : α) in , f x = ∑ (x : α) in s, f x
theorem finset.prod_filter_ne_one {β : Type u} {α : Type v} {s : finset α} {f : α → β} [comm_monoid β] [Π (x : α), decidable (f x 1)] :
∏ (x : α) in finset.filter (λ (x : α), f x 1) s, f x = ∏ (x : α) in s, f x
theorem finset.sum_filter_ne_zero {β : Type u} {α : Type v} {s : finset α} {f : α → β} [Π (x : α), decidable (f x 0)] :
∑ (x : α) in finset.filter (λ (x : α), f x 0) s, f x = ∑ (x : α) in s, f x
theorem finset.prod_filter {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] (p : α → Prop) (f : α → β) :
∏ (a : α) in , f a = ∏ (a : α) in s, ite (p a) (f a) 1
theorem finset.sum_filter {β : Type u} {α : Type v} {s : finset α} (p : α → Prop) (f : α → β) :
∑ (a : α) in , f a = ∑ (a : α) in s, 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) :
∏ (x : α) in s, 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) :
∑ (x : α) in s, 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) :
∑ (x : α) in s, 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) :
∏ (x : α) in s, 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) :
∏ (x : α) in s, 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) :
∑ (x : α) in s, 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) :
∏ (x : α) in s, 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) :
∑ (x : α) in s, f x = f a + f b
theorem finset.prod_attach {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] {f : α → β} :
∏ (x : {x // x s}) in s.attach, f x = ∏ (x : α) in s, f x
theorem finset.sum_attach {β : Type u} {α : Type v} {s : finset α} {f : α → β} :
∑ (x : {x // x s}) in s.attach, f x = ∑ (x : α) in s, f x
@[simp]
theorem finset.prod_subtype_eq_prod_filter {β : Type u} {α : Type v} {s : finset α} [comm_monoid β] (f : α → β) {p : α → Prop}  :
∏ (x : subtype p) in , f x = ∏ (x : α) in , 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}  :
∑ (x : subtype p) in , f x = ∑ (x : α) in , 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) :
∏ (x : subtype p) in , f x = ∏ (x : α) in s, 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) :
∑ (x : subtype p) in , f x = ∑ (x : α) in s, 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) :
∑ (x : α) in finset.map (function.embedding.subtype (λ (x : α), p x)) s, g x = ∑ (x : {x // p x}) in s, 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) :
∏ (x : α) in finset.map (function.embedding.subtype (λ (x : α), p x)) s, g x = ∏ (x : {x // p x}) in s, 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.prod_finset_coe {β : Type u} {α : Type v} [comm_monoid β] (f : α → β) (s : finset α) :
∏ (i : s), f i = ∏ (i : α) in s, f i
theorem finset.sum_finset_coe {β : Type u} {α : Type v} (f : α → β) (s : finset α) :
∑ (i : s), f i = ∑ (i : α) in s, 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 : α → β) :
∏ (a : α) in s, f a = ∏ (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 : α → β) :
∑ (a : α) in s, f a = ∑ (a : subtype p), f a
theorem finset.sum_eq_zero {β : Type u} {α : Type v} {f : α → β} {s : finset α} (h : ∀ (x : α), x sf x = 0) :
∑ (x : α) in s, f x = 0
theorem finset.prod_eq_one {β : Type u} {α : Type v} [comm_monoid β] {f : α → β} {s : finset α} (h : ∀ (x : α), x sf x = 1) :
∏ (x : α) in s, f x = 1
theorem finset.prod_apply_dite {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] {s : finset α} {p : α → Prop} {hp : decidable_pred p} (f : Π (x : α), p x → γ) (g : Π (x : α), ¬p x → γ) (h : γ → β) :
∏ (x : α) in s, h (dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx)) = (∏ (x : {x // x s}) in s).attach, h (f x.val _)) * ∏ (x : {x // x finset.filter (λ (x : α), ¬p x) s}) in (finset.filter (λ (x : α), ¬p x) s).attach, h (g x.val _)
theorem finset.sum_apply_dite {β : Type u} {α : Type v} {γ : Type w} {s : finset α} {p : α → Prop} {hp : decidable_pred p} (f : Π (x : α), p x → γ) (g : Π (x : α), ¬p x → γ) (h : γ → β) :
∑ (x : α) in s, h (dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx)) = ∑ (x : {x // x s}) in s).attach, h (f x.val _) + ∑ (x : {x // x finset.filter (λ (x : α), ¬p x) s}) in (finset.filter (λ (x : α), ¬p x) s).attach, 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 : γ → β) :
∏ (x : α) in s, h (ite (p x) (f x) (g x)) = (∏ (x : α) in , h (f x)) * ∏ (x : α) in finset.filter (λ (x : α), ¬p x) s, 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 : γ → β) :
∑ (x : α) in s, h (ite (p x) (f x) (g x)) = ∑ (x : α) in , h (f x) + ∑ (x : α) in finset.filter (λ (x : α), ¬p x) s, 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 → β) :
∑ (x : α) in s, dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx) = ∑ (x : {x // x s}) in s).attach, f x.val _ + ∑ (x : {x // x finset.filter (λ (x : α), ¬p x) s}) in (finset.filter (λ (x : α), ¬p x) s).attach, 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 → β) :
∏ (x : α) in s, dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx) = (∏ (x : {x // x s}) in s).attach, f x.val _) * ∏ (x : {x // x finset.filter (λ (x : α), ¬p x) s}) in (finset.filter (λ (x : α), ¬p x) s).attach, g x.val _
theorem finset.prod_ite {β : Type u} {α : Type v} [comm_monoid β] {s : finset α} {p : α → Prop} {hp : decidable_pred p} (f g : α → β) :
∏ (x : α) in s, ite (p x) (f x) (g x) = (∏ (x : α) in , f x) * ∏ (x : α) in finset.filter (λ (x : α), ¬p x) s, g x
theorem finset.sum_ite {β : Type u} {α : Type v} {s : finset α} {p : α → Prop} {hp : decidable_pred p} (f g : α → β) :
∑ (x : α) in s, ite (p x) (f x) (g x) = ∑ (x : α) in , f x + ∑ (x : α) in finset.filter (λ (x : α), ¬p x) s, 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) :
∏ (x : α) in s, ite (p x) (f x) (g x) = ∏ (x : α) in s, 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) :
∑ (x : α) in s, ite (p x) (f x) (g x) = ∑ (x : α) in s, 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) :
∏ (x : α) in s, ite (p x) (f x) (g x) = ∏ (x : α) in s, 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) :
∑ (x : α) in s, ite (p x) (f x) (g x) = ∑ (x : α) in s, 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) :
∑ (x : α) in s, k (ite (p x) (f x) (g x)) = ∑ (x : α) in s, 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) :
∏ (x : α) in s, k (ite (p x) (f x) (g x)) = ∏ (x : α) in s, 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) :
∑ (x : α) in s, k (ite (p x) (f x) (g x)) = ∑ (x : α) in s, 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) :
∏ (x : α) in s, k (ite (p x) (f x) (g x)) = ∏ (x : α) in s, k (f x)
theorem finset.sum_extend_by_zero {β : Type u} {α : Type v} [decidable_eq α] (s : finset α) (f : α → β) :
∑ (i : α) in s, ite (i s) (f i) 0 = ∑ (i : α) in s, f i
theorem finset.prod_extend_by_one {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s : finset α) (f : α → β) :
∏ (i : α) in s, ite (i s) (f i) 1 = ∏ (i : α) in s, f i
@[simp]
theorem finset.sum_dite_eq {β : Type u} {α : Type v} [decidable_eq α] (s : finset α) (a : α) (b : Π (x : α), a = x → β) :
∑ (x : α) in s, 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 → β) :
∏ (x : α) in s, 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 → β) :
∏ (x : α) in s, 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 → β) :
∑ (x : α) in s, 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 : α → β) :
∏ (x : α) in s, 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 : α → β) :
∑ (x : α) in s, 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 : α → β) :
∑ (x : α) in s, ite (x = a) (b x) 0 = ite (a s) (b a) 0
@[simp]
theorem finset.prod_ite_eq' {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s : finset α) (a : α) (b : α → β) :
∏ (x : α) in s, ite (x = a) (b x) 1 = ite (a s) (b a) 1

When a product is taken over a conditional whose condition is an equality test on the index and whose alternative is 1, then the product's value is either the term at that index or `1`.

The difference with `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 : α → β) :
∑ (x : α) in ite p s t, f x = ite p (∑ (x : α) in s, f x) (∑ (x : α) in t, f x)
theorem finset.prod_ite_index {β : Type u} {α : Type v} [comm_monoid β] (p : Prop) [decidable p] (s t : finset α) (f : α → β) :
∏ (x : α) in ite p s t, f x = ite p (∏ (x : α) in s, f x) (∏ (x : α) in t, f x)
@[simp]
theorem finset.sum_dite_irrel {β : Type u} {α : Type v} (p : Prop) [decidable p] (s : finset α) (f : p → α → β) (g : ¬p → α → β) :
∑ (x : α) in s, dite p (λ (h : p), f h x) (λ (h : ¬p), g h x) = dite p (λ (h : p), ∑ (x : α) in s, f h x) (λ (h : ¬p), ∑ (x : α) in s, 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 → α → β) :
∏ (x : α) in s, dite p (λ (h : p), f h x) (λ (h : ¬p), g h x) = dite p (λ (h : p), ∏ (x : α) in s, f h x) (λ (h : ¬p), ∏ (x : α) in s, g h x)
@[simp]
theorem finset.sum_pi_single' {ι : Type u_1} {M : Type u_2} [decidable_eq ι] (i : ι) (x : M) (s : finset ι) :
∑ (j : ι) in s, 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 ι) :
∑ (j : ι) in s, (f j) i = ite (i s) (f i) 0
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)) :
∑ (x : α) in s, f x = ∑ (x : γ) in t, 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)) :
∏ (x : α) in s, f x = ∏ (x : γ) in t, 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) :
∑ (x : α) in s, f x = ∑ (x : γ) in t, 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) :
∏ (x : α) in s, f x = ∏ (x : γ) in t, 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.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₂)) :
∏ (x : α) in s, f x = ∏ (x : γ) in t, 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₂)) :
∑ (x : α) in s, f x = ∑ (x : γ) in t, g x
theorem finset.nonempty_of_sum_ne_zero {β : Type u} {α : Type v} {s : finset α} {f : α → β} (h : ∑ (x : α) in s, f x 0) :
theorem finset.nonempty_of_prod_ne_one {β : Type u} {α : Type v} {s : finset α} {f : α → β} [comm_monoid β] (h : ∏ (x : α) in s, f x 1) :
theorem finset.exists_ne_zero_of_sum_ne_zero {β : Type u} {α : Type v} {s : finset α} {f : α → β} (h : ∑ (x : α) in s, 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 : ∏ (x : α) in s, f x 1) :
∃ (a : α) (H : a s), f a 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) :
∑ (i : α) in s₁, f i = ∑ (i : α) in s₂, 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) :
∏ (i : α) in s₁, f i = ∏ (i : α) in s₂, g i
theorem finset.prod_range_succ_comm {β : Type u} [comm_monoid β] (f : → β) (n : ) :
∏ (x : ) in finset.range (n + 1), f x = (f n) * ∏ (x : ) in , f x
theorem finset.sum_range_succ_comm {β : Type u} (f : → β) (n : ) :
∑ (x : ) in finset.range (n + 1), f x = f n + ∑ (x : ) in , f x
theorem finset.prod_range_succ {β : Type u} [comm_monoid β] (f : → β) (n : ) :
∏ (x : ) in finset.range (n + 1), f x = (∏ (x : ) in , f x) * f n
theorem finset.sum_range_succ {β : Type u} (f : → β) (n : ) :
∑ (x : ) in finset.range (n + 1), f x = ∑ (x : ) in , f x + f n
theorem finset.prod_range_succ' {β : Type u} [comm_monoid β] (f : → β) (n : ) :
∏ (k : ) in finset.range (n + 1), f k = (∏ (k : ) in , f (k + 1)) * f 0
theorem finset.sum_range_succ' {β : Type u} (f : → β) (n : ) :
∑ (k : ) in finset.range (n + 1), f k = ∑ (k : ) in , f (k + 1) + f 0
theorem finset.eventually_constant_sum {β : Type u} {u : → β} {N : } (hu : ∀ (n : ), n Nu n = 0) {n : } (hn : N n) :
∑ (k : ) in finset.range (n + 1), u k = ∑ (k : ) in finset.range (N + 1), u k
theorem finset.eventually_constant_prod {β : Type u} [comm_monoid β] {u : → β} {N : } (hu : ∀ (n : ), n Nu n = 1) {n : } (hn : N n) :
∏ (k : ) in finset.range (n + 1), u k = ∏ (k : ) in finset.range (N + 1), u k
theorem finset.prod_range_add {β : Type u} [comm_monoid β] (f : → β) (n m : ) :
∏ (x : ) in finset.range (n + m), f x = (∏ (x : ) in , f x) * ∏ (x : ) in , f (n + x)
theorem finset.sum_range_add {β : Type u} (f : → β) (n m : ) :
∑ (x : ) in finset.range (n + m), f x = ∑ (x : ) in , f x + ∑ (x : ) in , f (n + x)
theorem finset.sum_range_zero {β : Type u} (f : → β) :
∑ (k : ) in , f k = 0
theorem finset.prod_range_zero {β : Type u} [comm_monoid β] (f : → β) :
∏ (k : ) in , f k = 1
theorem finset.sum_range_one {β : Type u} (f : → β) :
∑ (k : ) in , f k = f 0
theorem finset.prod_range_one {β : Type u} [comm_monoid β] (f : → β) :
∏ (k : ) in , f k = f 0
theorem finset.prod_multiset_map_count {α : Type v} [decidable_eq α] (s : multiset α) {M : Type u_1} [comm_monoid M] (f : α → M) :
s).prod = ∏ (m : α) in s.to_finset, f m ^
theorem finset.sum_multiset_map_count {α : Type v} [decidable_eq α] (s : multiset α) {M : Type u_1} (f : α → M) :
s).sum = ∑ (m : α) in s.to_finset, f m
theorem finset.sum_multiset_count {α : Type v} [decidable_eq α] (s : multiset α) :
s.sum = ∑ (m : α) in s.to_finset, m
theorem finset.prod_multiset_count {α : Type v} [decidable_eq α] [comm_monoid α] (s : multiset α) :
s.prod = ∏ (m : α) in s.to_finset, m ^
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 (∏ (x : α) in s, 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 (∑ (x : α) in s, 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 (∑ (x : α) in s, 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 (∏ (x : α) in s, f x)

To prove a property of a product, it suffices to prove that the property is multiplicative and holds on factors.

theorem finset.prod_range_induction {M : Type u_1} [comm_monoid M] (f s : → M) (h0 : s 0 = 1) (h : ∀ (n : ), s (n + 1) = (s n) * f n) (n : ) :
∏ (k : ) in , f k = s n

For any product along `{0, ..., n-1}` of a commutative-monoid-valued function, we can verify that it's equal to a different function just by checking ratios of adjacent terms. This is a multiplicative discrete analogue of the fundamental theorem of calculus.

theorem finset.sum_range_induction {M : Type u_1} (f s : → M) (h0 : s 0 = 0) (h : ∀ (n : ), s (n + 1) = s n + f n) (n : ) :
∑ (k : ) in , f k = s n

For any sum along `{0, ..., n-1}` of a commutative-monoid-valued function, we can verify that it's equal to a different function just by checking differences of adjacent terms. This is a discrete analogue of the fundamental theorem of calculus.

theorem finset.sum_range_sub {G : Type u_1} (f : → G) (n : ) :
∑ (i : ) in , (f (i + 1) - f i) = f n - f 0

A telescoping sum along `{0, ..., n-1}` of an additive commutative group valued function reduces to the difference of the last and first terms.

theorem finset.sum_range_sub' {G : Type u_1} (f : → G) (n : ) :
∑ (i : ) in , (f i - f (i + 1)) = f 0 - f n
theorem finset.prod_range_div {M : Type u_1} [comm_group M] (f : → M) (n : ) :
∏ (i : ) in , (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 : ) :
∏ (i : ) in , (f i) * (f (i + 1))⁻¹ = (f 0) * (f n)⁻¹
theorem finset.sum_range_sub_of_monotone {f : } (h : monotone f) (n : ) :
∑ (i : ) in , (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 : β) :
∏ (x : α) in s, b = b ^ s.card
theorem finset.pow_eq_prod_const {β : Type u} [comm_monoid β] (b : β) (n : ) :
b ^ n = ∏ (k : ) in , b
theorem finset.prod_pow {β : Type u} {α : Type v} [comm_monoid β] (s : finset α) (n : ) (f : α → β) :
∏ (x : α) in s, f x ^ n = (∏ (x : α) in s, f x) ^ n
theorem finset.prod_flip {β : Type u} [comm_monoid β] {n : } (f : → β) :
∏ (r : ) in finset.range (n + 1), f (n - r) = ∏ (k : ) in finset.range (n + 1), f k
theorem finset.sum_flip {β : Type u} {n : } (f : → β) :
∑ (r : ) in finset.range (n + 1), f (n - r) = ∑ (k : ) in finset.range (n + 1), 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) :
∏ (x : α) in s, 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) :
∑ (x : α) in s, f x = 0
theorem finset.prod_comp {β : Type u} {α : Type v} {γ : Type w} [comm_monoid β] [decidable_eq γ] {s : finset α} (f : γ → β) (g : α → γ) :
∏ (a : α) in s, f (g a) = ∏ (b : γ) in s, 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`

theorem finset.sum_piecewise {β : Type u} {α : Type v} [decidable_eq α] (s t : finset α) (f g : α → β) :
∑ (x : α) in s, t.piecewise f g x = ∑ (x : α) in s t, f x + ∑ (x : α) in s \ t, g x
theorem finset.prod_piecewise {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s t : finset α) (f g : α → β) :
∏ (x : α) in s, t.piecewise f g x = (∏ (x : α) in s t, f x) * ∏ (x : α) in s \ t, g x
theorem finset.prod_inter_mul_prod_diff {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s t : finset α) (f : α → β) :
(∏ (x : α) in s t, f x) * ∏ (x : α) in s \ t, f x = ∏ (x : α) in s, f x
theorem finset.sum_inter_add_sum_diff {β : Type u} {α : Type v} [decidable_eq α] (s t : finset α) (f : α → β) :
∑ (x : α) in s t, f x + ∑ (x : α) in s \ t, f x = ∑ (x : α) in s, 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 : α → β) :
∏ (x : α) in s, f x = (f i) * ∏ (x : α) in s \ {i}, f x
theorem finset.sum_eq_add_sum_diff_singleton {β : Type u} {α : Type v} [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α → β) :
∑ (x : α) in s, f x = f i + ∑ (x : α) in s \ {i}, 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 : α → β) :
∏ (x : α) in s, f x = (∏ (x : α) in s \ {i}, 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 : α → β) :
∑ (x : α) in s, f x = ∑ (x : α) in s \ {i}, f x + f i
theorem fintype.prod_eq_mul_prod_compl {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] [fintype α] (a : α) (f : α → β) :
∏ (i : α), f i = (f a) * ∏ (i : α) in {a}, f i
theorem fintype.sum_eq_add_sum_compl {β : Type u} {α : Type v} [decidable_eq α] [fintype α] (a : α) (f : α → β) :
∑ (i : α), f i = f a + ∑ (i : α) in {a}, f i
theorem fintype.prod_eq_prod_compl_mul {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] [fintype α] (a : α) (f : α → β) :
∏ (i : α), f i = (∏ (i : α) in {a}, f i) * f a
theorem fintype.sum_eq_sum_compl_add {β : Type u} {α : Type v} [decidable_eq α] [fintype α] (a : α) (f : α → β) :
∑ (i : α), f i = ∑ (i : α) in {a}, f i + f a
theorem finset.sum_partition {β : Type u} {α : Type v} {s : finset α} {f : α → β} (R : setoid α)  :
∑ (x : α) in s, f x = ∑ (xbar : quotient R) in , ∑ (y : α) in finset.filter (λ (y : α), y = xbar) s, 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 α)  :
∏ (x : α) in s, f x = ∏ (xbar : quotient R) in , ∏ (y : α) in finset.filter (λ (y : α), y = xbar) s, 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∏ (a : α) in finset.filter (λ (y : α), y x) s, f a = 1) :
∏ (x : α) in s, 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∑ (a : α) in finset.filter (λ (y : α), y x) s, f a = 0) :
∑ (x : α) in s, 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 : β) :
∏ (x : α) in s, b x = ∏ (x : α) in s, f x
theorem finset.sum_update_of_not_mem {β : Type u} {α : Type v} [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α → β) (b : β) :
∑ (x : α) in s, b x = ∑ (x : α) in s, f x
theorem finset.prod_update_of_mem {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α → β) (b : β) :
∏ (x : α) in s, b x = b * ∏ (x : α) in s \ {i}, 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 : ∑ (x : α) in s, 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 : ∏ (x : α) in s, 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.prod_erase {β : Type u} {α : Type v} [comm_monoid β] [decidable_eq α] (s : finset α) {f : α → β} {a : α} (h : f a = 1) :
∏ (x : α) in s.erase a, f x = ∏ (x : α) in s, 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) :
∑ (x : α) in s.erase a, f x = ∑ (x : α) in s, 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.eq_zero_of_sum_eq_zero {β : Type u} {α : Type v} {s : finset α} {f : α → β} {a : α} (hp : ∑ (x : α) in s, 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 : ∏ (x : α) in s, 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 : α) :
∏ (x : α) in s, f x ^ ite (a = x) 1 0 = ite (a s) (f a) 1
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) :
∏ (i : α) in s, g i + ∏ (i : α) in s, h i = ∏ (i : α) in s, 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.sum_update_of_mem {β : Type u} {α : Type v} [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α → β) (b : β) :
∑ (x : α) in s, b x = b + ∑ (x : α) in s \ {i}, f x
theorem finset.sum_nsmul {β : Type u} {α : Type v} (s : finset α) (n : ) (f : α → β) :
∑ (x : α) in s, n f x = n ∑ (x : α) in s, f x
@[simp]
theorem finset.sum_const {β : Type u} {α : Type v} {s : finset α} (b : β) :
∑ (x : α) in s, b = s.card b
theorem finset.card_eq_sum_ones {α : Type v} (s : finset α) :
s.card = ∑ (_x : α) in s, 1
theorem finset.sum_const_nat {α : Type v} {s : finset α} {m : } {f : α → } (h₁ : ∀ (x : α), x sf x = m) :
∑ (x : α) in s, f x = (s.card) * m
@[simp]
theorem finset.sum_boole {β : Type u} {α : Type v} {s : finset α} {p : α → Prop} {hp : decidable_pred p} :
∑ (x : α) in s, ite (p x) 1 0 = s).card)
theorem finset.sum_comp {β : Type u} {α : Type v} {γ : Type w} [decidable_eq γ] {s : finset α} (f : γ → β) (g : α → γ) :
∑ (a : α) in s, f (g a) = ∑ (b : γ) in s, (finset.filter (λ (a : α), g a = b) s).card f b
theorem finset.eq_sum_range_sub {β : Type u} (f : → β) (n : ) :
f n = f 0 + ∑ (i : ) in , (f (i + 1) - f i)
theorem finset.eq_sum_range_sub' {β : Type u} (f : → β) (n : ) :
f n = ∑ (i : ) in finset.range (n + 1), ite (i = 0) (f 0) (f i - f (i - 1))
@[simp]
theorem finset.op_sum {β : Type u} {α : Type v} {s : finset α} (f : α → β) :
opposite.op (∑ (x : α) in s, f x) = ∑ (x : α) in s, 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 : α → βᵒᵖ) :
opposite.unop (∑ (x : α) in s, f x) = ∑ (x : α) in s, opposite.unop (f x)
@[simp]
theorem finset.sum_neg_distrib {β : Type u} {α : Type v} {s : finset α} {f : α → β}  :
∑ (x : α) in s, -f x = -∑ (x : α) in s, f x
@[simp]
theorem finset.prod_inv_distrib {β : Type u} {α : Type v} {s : finset α} {f : α → β} [comm_group β] :
∏ (x : α) in s, (f x)⁻¹ = (∏ (x : α) in s, f x)⁻¹
@[simp]
theorem finset.card_sigma {α : Type v} {σ : α → Type u_1} (s : finset α) (t : Π (a : α), finset (σ a)) :
(s.sigma t).card = ∑ (a : α) in s, (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 = ∑ (u : α) in s, (t u).card
theorem finset.card_bUnion_le {β : Type u} {α : Type v} [decidable_eq β] {s : finset α} {t : α → } :
(s.bUnion t).card ∑ (a : α) in s, (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 = ∑ (a : β) in t, (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 = ∑ (a : β) in s, (finset.filter (λ (x : α), f x = a) s).card
theorem finset.gsmul_sum {β : Type u} {α : Type v} {f : α → β} {s : finset α} (z : ) :
(∑ (a : α) in s, f a) = ∑ (a : α) in s, (f a)
@[simp]
theorem finset.sum_sub_distrib {β : Type u} {α : Type v} {s : finset α} {f g : α → β}  :
∑ (x : α) in s, (f x - g x) = ∑ (x : α) in s, f x - ∑ (x : α) in s, g x
theorem finset.prod_eq_zero {β : Type u} {α : Type v} {s : finset α} {a : α} {f : α → β} (ha : a s) (h : f a = 0) :
∏ (x : α) in s, f x = 0
theorem finset.prod_boole {β : Type u} {α : Type v} {s : finset α} {p : α → Prop}  :
∏ (i : α) in s, 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 β]  :
∏ (x : α) in s, f x = 0 ∃ (a : α) (H : a s), f a = 0
theorem finset.prod_ne_zero_iff {β : Type u} {α : Type v} {s : finset α} {f : α → β} [nontrivial β]  :
∏ (x : α) in s, f x 0 ∀ (a : α), a sf a 0
@[simp]
theorem finset.prod_inv_distrib' {β : Type u} {α : Type v} {s : finset α} {f : α → β}  :
∏ (x : α) in s, (f x)⁻¹ = (∏ (x : α) in s, 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)) :
∑ (x : α), f x = ∑ (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)) :
∏ (x : α), f x = ∏ (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)) :
∏ (x : α), f x = ∏ (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)) :
∑ (x : α), f x = ∑ (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.prod_finset_coe {β : Type u} {α : Type v} {s : finset α} {f : α → β} [comm_monoid β] :
∏ (i : s), f i = ∏ (i : α) in s, f i
theorem fintype.sum_finset_coe {β : Type u} {α : Type v} {s : finset α} {f : α → β}  :
∑ (i : s), f i = ∑ (i : α) in s, 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.abs_sum_le_sum_abs {α : Type v} {s : multiset α} :
abs s.sum s).sum
@[simp]
theorem multiset.to_finset_sum_count_eq {α : Type v} [decidable_eq α] (s : multiset α) :
∑ (a : α) in s.to_finset, =
theorem multiset.count_sum' {β : Type u} {α : Type v} [decidable_eq α] {s : finset β} {a : α} {f : β → } :
(∑ (x : β) in s, f x) = ∑ (x : β) in s, (f x)
@[simp]
theorem multiset.to_finset_sum_count_nsmul_eq {α : Type v} [decidable_eq α] (s : multiset α) :
∑ (a : α) in s.to_finset, (a ::ₘ 0) = s
theorem multiset.exists_smul_of_dvd_count {α : Type v} [decidable_eq α] (s : multiset α) {k : } (h : ∀ (a : α), k ) :
∃ (u : multiset α), s = k u
@[simp]
theorem nat.cast_sum {β : Type u} {α : Type v} [has_one β] (s : finset α) (f : α → ) :
∑ (x : α) in s, f x = ∑ (x : α) in s, (f x)
@[simp]
theorem int.cast_sum {β : Type u} {α : Type v} [has_one β] (s : finset α) (f : α → ) :
∑ (x : α) in s, f x = ∑ (x : α) in s, (f x)
@[simp]
theorem nat.cast_prod {α : Type v} {R : Type u_1} (f : α → ) (s : finset α) :
∏ (i : α) in s, f i = ∏ (i : α) in s, (f i)
@[simp]
theorem int.cast_prod {α : Type v} {R : Type u_1} [comm_ring R] (f : α → ) (s : finset α) :
∏ (i : α) in s, f i = ∏ (i : α) in s, (f i)
@[simp]
theorem units.coe_prod {α : Type v} {M : Type u_1} [comm_monoid M] (f : α → ) (s : finset α) :
∏ (i : α) in s, f i = ∏ (i : α) in s, (f i)
theorem nat_abs_sum_le {ι : Type u_1} (s : finset ι) (f : ι → ) :
(∑ (i : ι) in s, f i).nat_abs ∑ (i : ι) in s, (f i).nat_abs