mathlib documentation

algebra.big_operators.basic

Big operators

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

Notation

We introduce the following notation, localized in big_operators. To enable the notation, use open_locale big_operators.

Let s be a finset α, and f : α → β a function.

def finset.sum {α : Type u} {β : Type v} [add_comm_monoid β] (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 = (multiset.map f s).prod

@[simp]
theorem finset.sum_mk {α : Type u} {β : Type v} [add_comm_monoid β] (s : multiset α) (hs : s.nodup) (f : α → β) :
{val := s, nodup := hs}.sum f = (multiset.map f s).sum

theorem finset.prod_eq_multiset_prod {α : Type u} {β : Type v} [comm_monoid β] (s : finset α) (f : α → β) :
∏ (x : α) in s, f x = (multiset.map f s.val).prod

theorem finset.sum_eq_multiset_sum {α : Type u} {β : Type v} [add_comm_monoid β] (s : finset α) (f : α → β) :
∑ (x : α) in s, f x = (multiset.map f s.val).sum

theorem finset.prod_eq_fold {α : Type u} {β : Type v} [comm_monoid β] (s : finset α) (f : α → β) :
∏ (x : α) in s, f x = finset.fold has_mul.mul 1 f s

theorem finset.sum_eq_fold {α : Type u} {β : Type v} [add_comm_monoid β] (s : finset α) (f : α → β) :
∑ (x : α) in s, f x = finset.fold has_add.add 0 f s

theorem add_monoid_hom.map_sum {α : Type u} {β : Type v} {γ : Type w} [add_comm_monoid β] [add_comm_monoid γ] (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} [add_comm_monoid β] [add_comm_monoid γ] (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 v} {γ : Type w} [semiring β] [semiring γ] (f : β →+* γ) (l : list β) :

theorem ring_hom.map_list_sum {β : Type v} {γ : Type w} [semiring β] [semiring γ] (f : β →+* γ) (l : list β) :

theorem ring_hom.map_multiset_prod {β : Type v} {γ : Type w} [comm_semiring β] [comm_semiring γ] (f : β →+* γ) (s : multiset β) :

theorem ring_hom.map_multiset_sum {β : Type v} {γ : Type w} [semiring β] [semiring γ] (f : β →+* γ) (s : multiset β) :

theorem ring_hom.map_prod {α : Type u} {β : Type v} {γ : Type w} [comm_semiring β] [comm_semiring γ] (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} [semiring β] [semiring γ] (g : β →+* γ) (f : α → β) (s : finset α) :
g (∑ (x : α) in s, f x) = ∑ (x : α) in s, g (f x)

@[simp]
theorem finset.sum_empty {β : Type v} [add_comm_monoid β] {α : Type u} {f : α → β} :
∑ (x : α) in , f x = 0

@[simp]
theorem finset.prod_empty {β : Type v} [comm_monoid β] {α : Type u} {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 insert a s, f x = (f a) * ∏ (x : α) in s, f x

@[simp]
theorem finset.sum_insert {α : Type u} {β : Type v} {s : finset α} {a : α} {f : α → β} [add_comm_monoid β] [decidable_eq α] :
a s∑ (x : α) in insert a 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 : α → β} [add_comm_monoid β] [decidable_eq α] (h : a sf a = 0) :
∑ (x : α) in insert a 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 insert a 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 : α → β} [add_comm_monoid β] [decidable_eq α] (h : f a = 0) :
∑ (x : α) in insert a 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 insert a 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 : α → β} [add_comm_monoid β] :
∑ (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 : α → β} [add_comm_monoid β] [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 u_1} {s : finset α} [add_comm_monoid β] :
∑ (x : α) in s, 0 = 0

@[simp]
theorem finset.sum_image {α : Type u} {β : Type v} {γ : Type w} {f : α → β} [add_comm_monoid β] [decidable_eq α] {s : finset γ} {g : γ → α} :
(∀ (x : γ), x s∀ (y : γ), y sg x = g yx = y)∑ (x : α) in finset.image g 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 finset.image g s, f x = ∏ (x : γ) in s, f (g x)

@[simp]
theorem finset.sum_map {α : Type u} {β : Type v} {γ : Type w} [add_comm_monoid β] (s : finset α) (e : α γ) (f : γ → β) :
∑ (x : γ) in finset.map e 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 finset.map e 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 : α → β} [add_comm_monoid β] (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 : α → β} [add_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_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 : α → β} [add_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.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 : α → β} [add_comm_monoid β] [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} [add_comm_monoid β] [decidable_eq γ)] (s : finset α) (t : finset γ) (f : α → β) (g : γ → β) :
∑ (x : α γ) in finset.image sum.inl s finset.image sum.inr t, sum.elim f 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 finset.image sum.inl s finset.image sum.inr t, sum.elim f g x = (∏ (x : α) in s, f x) * ∏ (x : γ) in t, g x

theorem finset.sum_bind {α : Type u} {β : Type v} {γ : Type w} {f : α → β} [add_comm_monoid β] [decidable_eq α] {s : finset γ} {t : γ → finset α} :
(∀ (x : γ), x s∀ (y : γ), y sx ydisjoint (t x) (t y))∑ (x : α) in s.bind t, f x = ∑ (x : γ) in s, ∑ (i : α) in t x, f i

theorem finset.prod_bind {α : Type u} {β : Type v} {γ : Type w} {f : α → β} [comm_monoid β] [decidable_eq α] {s : finset γ} {t : γ → finset α} :
(∀ (x : γ), x s∀ (y : γ), y sx ydisjoint (t x) (t y))∏ (x : α) in s.bind 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} [add_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} [add_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.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 : sigma σ → β) :
∏ (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} [add_comm_monoid β] {σ : α → Type u_1} (s : finset α) (t : Π (a : α), finset (σ a)) (f : sigma σ → β) :
∑ (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} [add_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_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} [add_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.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 finset.image g s, f x = ∏ (x : γ) in s, h x

theorem finset.sum_image' {α : Type u} {β : Type v} {γ : Type w} {f : α → β} [add_comm_monoid β] [decidable_eq α] {s : finset γ} {g : γ → α} (h : γ → β) (eq : ∀ (c : γ), c sf (g c) = ∑ (x : γ) in finset.filter (λ (c' : γ), g c' = g c) s, h x) :
∑ (x : α) in finset.image g 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 : α → β} [add_comm_monoid β] :
∑ (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} [add_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.prod_hom {α : Type u} {β : Type v} {γ : Type w} [comm_monoid β] [comm_monoid γ] (s : finset α) {f : α → β} (g : β → γ) [is_monoid_hom g] :
∏ (x : α) in s, g (f x) = g (∏ (x : α) in s, f x)

theorem finset.sum_hom {α : Type u} {β : Type v} {γ : Type w} [add_comm_monoid β] [add_comm_monoid γ] (s : finset α) {f : α → β} (g : β → γ) [is_add_monoid_hom g] :
∑ (x : α) in s, g (f x) = g (∑ (x : α) in s, f x)

theorem finset.sum_hom_rel {α : Type u} {β : Type v} {γ : Type w} [add_comm_monoid β] [add_comm_monoid γ] {r : β → γ → Prop} {f : α → β} {g : α → γ} {s : finset α} (h₁ : r 0 0) (h₂ : ∀ (a : α) (b : β) (c : γ), r b cr (f a + b) (g a + c)) :
r (∑ (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 : α → β} [add_comm_monoid β] (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} [decidable_pred p] (hp : ∀ (x : α), x sf x 1p x) :
∏ (x : α) in finset.filter p s, f x = ∏ (x : α) in s, f x

theorem finset.sum_filter_of_ne {α : Type u} {β : Type v} {s : finset α} {f : α → β} [add_comm_monoid β] {p : α → Prop} [decidable_pred p] (hp : ∀ (x : α), x sf x 0p x) :
∑ (x : α) in finset.filter p s, 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 : α → β} [add_comm_monoid β] [Π (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) [decidable_pred p] (f : α → β) :
∏ (a : α) in finset.filter p s, f a = ∏ (a : α) in s, ite (p a) (f a) 1

theorem finset.sum_filter {α : Type u} {β : Type v} {s : finset α} [add_comm_monoid β] (p : α → Prop) [decidable_pred p] (f : α → β) :
∑ (a : α) in finset.filter p s, f a = ∑ (a : α) in s, ite (p a) (f a) 0

theorem finset.sum_eq_single {α : Type u} {β : Type v} [add_comm_monoid β] {s : finset α} {f : α → β} (a : α) (h₀ : ∀ (b : α), b sb af b = 0) (h₁ : a sf a = 0) :
∑ (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_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 α} [add_comm_monoid β] {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} [decidable_pred p] :
∏ (x : subtype p) in finset.subtype p s, f x = ∏ (x : α) in finset.filter p s, f x

A product over s.subtype p equals one over s.filter p.

@[simp]
theorem finset.sum_subtype_eq_sum_filter {α : Type u} {β : Type v} {s : finset α} [add_comm_monoid β] (f : α → β) {p : α → Prop} [decidable_pred p] :
∑ (x : subtype p) in finset.subtype p s, f x = ∑ (x : α) in finset.filter p s, f x

A sum over s.subtype p equals one over s.filter p.

theorem finset.prod_subtype_of_mem {α : Type u} {β : Type v} {s : finset α} [comm_monoid β] (f : α → β) {p : α → Prop} [decidable_pred p] (h : ∀ (x : α), x sp x) :
∏ (x : subtype p) in finset.subtype p s, 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 α} [add_comm_monoid β] (f : α → β) {p : α → Prop} [decidable_pred p] (h : ∀ (x : α), x sp x) :
∑ (x : subtype p) in finset.subtype p s, 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} [add_comm_monoid β] {p : α → Prop} {s : finset {x // p x}} {f : {x // p x} → β} {g : α → β} (h : ∀ (x : {x // p x}), x sg x = f x) :
∑ (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.sum_eq_zero {α : Type u} {β : Type v} [add_comm_monoid β] {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 finset.filter p s}) in (finset.filter p 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} [add_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 finset.filter p s}) in (finset.filter p 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 finset.filter p s, 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} [add_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 finset.filter p s, h (f x) + ∑ (x : α) in finset.filter (λ (x : α), ¬p x) s, h (g x)

theorem finset.sum_dite {α : Type u} {β : Type v} [add_comm_monoid β] {s : finset α} {p : α → Prop} {hp : decidable_pred p} (f : Π (x : α), p x → β) (g : Π (x : α), ¬p x → β) :
∑ (x : α) in s, dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx) = ∑ (x : {x // x finset.filter p s}) in (finset.filter p 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 finset.filter p s}) in (finset.filter p 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 finset.filter p s, f x) * ∏ (x : α) in finset.filter (λ (x : α), ¬p x) s, g x

theorem finset.sum_ite {α : Type u} {β : Type v} [add_comm_monoid β] {s : finset α} {p : α → Prop} {hp : decidable_pred p} (f g : α → β) :
∑ (x : α) in s, ite (p x) (f x) (g x) = ∑ (x : α) in finset.filter p s, f x + ∑ (x : α) in finset.filter (λ (x : α), ¬p x) s, g x

theorem finset.sum_extend_by_zero {α : Type u} {β : Type v} [add_comm_monoid β] [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} [add_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), 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} [add_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), 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} [add_comm_monoid β] [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} [add_comm_monoid β] [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} [add_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)

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)

theorem finset.sum_bij {α : Type u} {β : Type v} {γ : Type w} [add_comm_monoid β] {s : finset α} {t : finset γ} {f : α → β} {g : γ → β} (i : Π (a : α), a s → γ) (hi : ∀ (a : α) (ha : a s), i a ha t) (h : ∀ (a : α) (ha : a s), f a = g (i a ha)) (i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ s) (ha₂ : a₂ s), i a₁ ha₁ = i a₂ ha₂a₁ = a₂) (i_surj : ∀ (b : γ), b t(∃ (a : α) (ha : a s), b = i a ha)) :
∑ (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} [add_comm_monoid β] {s : finset α} {t : finset γ} {f : α → β} {g : γ → β} (i : Π (a : α), a s → γ) (hi : ∀ (a : α) (ha : a s), i a ha t) (h : ∀ (a : α) (ha : a s), f a = g (i a ha)) (j : Π (a : γ), a t → α) (hj : ∀ (a : γ) (ha : a t), j a ha s) (left_inv : ∀ (a : α) (ha : a s), j (i a ha) _ = a) (right_inv : ∀ (a : γ) (ha : a t), i (j a ha) _ = a) :
∑ (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} [add_comm_monoid β] {s : finset α} {t : finset γ} {f : α → β} {g : γ → β} (i : Π (a : α), a sf a 0 → γ) (hi : ∀ (a : α) (h₁ : a s) (h₂ : f a 0), i a h₁ h₂ t) (i_inj : ∀ (a₁ a₂ : α) (h₁₁ : a₁ s) (h₁₂ : f a₁ 0) (h₂₁ : a₂ s) (h₂₂ : f a₂ 0), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂a₁ = a₂) (i_surj : ∀ (b : γ), b tg b 0(∃ (a : α) (h₁ : a s) (h₂ : f a 0), b = i a h₁ h₂)) (h : ∀ (a : α) (h₁ : a s) (h₂ : f a 0), f a = g (i a h₁ h₂)) :
∑ (x : α) in s, f x = ∑ (x : γ) in t, g x

theorem finset.nonempty_of_sum_ne_zero {α : Type u} {β : Type v} {s : finset α} {f : α → β} [add_comm_monoid β] (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 : α → β} [add_comm_monoid β] (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 : α → β} [add_comm_monoid β] [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.sum_range_succ {β : Type u_1} [add_comm_monoid β] (f : → β) (n : ) :
∑ (x : ) in finset.range (n + 1), f x = f n + ∑ (x : ) in finset.range n, f x

theorem finset.prod_range_succ {β : Type v} [comm_monoid β] (f : → β) (n : ) :
∏ (x : ) in finset.range (n + 1), f x = (f n) * ∏ (x : ) in finset.range n, f x

theorem finset.prod_range_succ' {β : Type v} [comm_monoid β] (f : → β) (n : ) :
∏ (k : ) in finset.range (n + 1), f k = (∏ (k : ) in finset.range n, f (k + 1)) * f 0

theorem finset.sum_range_zero {β : Type v} [add_comm_monoid β] (f : → β) :
∑ (k : ) in finset.range 0, f k = 0

theorem finset.prod_range_zero {β : Type v} [comm_monoid β] (f : → β) :
∏ (k : ) in finset.range 0, f k = 1

theorem finset.prod_range_one {β : Type v} [comm_monoid β] (f : → β) :
∏ (k : ) in finset.range 1, f k = f 0

theorem finset.sum_range_one {δ : Type u_1} [add_comm_monoid δ] (f : → δ) :
∑ (k : ) in finset.range 1, f k = f 0

theorem finset.prod_multiset_map_count {α : Type u} [decidable_eq α] (s : multiset α) {M : Type u_1} [comm_monoid M] (f : α → M) :
(multiset.map f s).prod = ∏ (m : α) in s.to_finset, f m ^ multiset.count m s

theorem finset.prod_multiset_count {α : Type u} [decidable_eq α] [comm_monoid α] (s : multiset α) :
s.prod = ∏ (m : α) in s.to_finset, m ^ multiset.count m s

theorem finset.prod_induction {α : Type u} {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 u} {s : finset α} {M : Type u_1} [add_comm_monoid M] (f : α → M) (p : M → Prop) (p_mul : ∀ (a b : M), p ap bp (a + b)) (p_one : p 0) (p_s : ∀ (x : α), x sp (f x)) :
p (∑ (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_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 finset.range n, f k = s n

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

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

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

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

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

theorem finset.sum_range_sub' {G : Type u_1} [add_comm_group G] (f : → G) (n : ) :
∑ (i : ) in finset.range n, (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 finset.range n, (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 finset.range n, (f i) * (f (i + 1))⁻¹ = (f 0) * (f n)⁻¹

theorem finset.sum_range_sub_of_monotone {f : } (h : monotone f) (n : ) :
∑ (i : ) in finset.range n, (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 v} [comm_monoid β] (b : β) (n : ) :
b ^ n = ∏ (k : ) in finset.range n, 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 v} [comm_monoid β] {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} [add_comm_monoid β] {s : finset α} {f : α → β} (g : Π (a : α), a s → α) (h : ∀ (a : α) (ha : a s), f a + f (g a ha) = 0) (g_ne : ∀ (a : α) (ha : a s), f a 0g a ha a) (g_mem : ∀ (a : α) (ha : a s), g a ha s) (g_inv : ∀ (a : α) (ha : a s), g (g a ha) _ = a) :
∑ (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 finset.image g 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} [add_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_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} [add_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.add_sum_diff_singleton {α : Type u} {β : Type v} [add_comm_monoid β] [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α → β) :
f i + ∑ (x : α) in s \ {i}, f x = ∑ (x : α) in s, f x

theorem finset.mul_prod_diff_singleton {α : Type u} {β : Type v} [comm_monoid β] [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α → β) :
(f i) * ∏ (x : α) in s \ {i}, f x = ∏ (x : α) in s, f x

theorem finset.sum_partition {α : Type u} {β : Type v} {s : finset α} {f : α → β} [add_comm_monoid β] (R : setoid α) [decidable_rel setoid.r] :
∑ (x : α) in s, f x = ∑ (xbar : quotient R) in finset.image quotient.mk s, ∑ (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 α) [decidable_rel setoid.r] :
∏ (x : α) in s, f x = ∏ (xbar : quotient R) in finset.image quotient.mk s, ∏ (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 α) [decidable_rel setoid.r] (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 : α → β} [add_comm_monoid β] (R : setoid α) [decidable_rel setoid.r] (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, function.update f i b x = ∏ (x : α) in s, f x

theorem finset.sum_update_of_not_mem {α : Type u} {β : Type v} [add_comm_monoid β] [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α → β) (b : β) :
∑ (x : α) in s, function.update f i 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, function.update f i b x = b * ∏ (x : α) in s \ {i}, f x

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.eq_of_card_le_one_of_sum_eq {α : Type u} {γ : Type w} [add_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 sum of a finset of size at most 1 has a given value, so do the terms in that sum.

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} [add_comm_monoid β] [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} [add_comm_monoid β] {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} [comm_semiring β] {s : finset α} {i : α} {f g h : α → β} (hi : i s) (h1 : g i + h i = f i) (h2 : ∀ (j : α), j sj ig j = f j) (h3 : ∀ (j : α), j sj ih j = f j) :
∏ (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} [add_comm_monoid β] [decidable_eq α] {s : finset α} {i : α} (h : i s) (f : α → β) (b : β) :
∑ (x : α) in s, function.update f i b x = b + ∑ (x : α) in s \ {i}, f x

theorem finset.sum_nsmul {α : Type u} {β : Type v} [add_comm_monoid β] (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 α} [add_comm_monoid β] (b : β) :
∑ (x : α) in s, b = s.card •ℕ b

theorem finset.card_eq_sum_ones {α : Type u} (s : finset α) :
s.card = ∑ (_x : α) in s, 1

theorem finset.sum_const_nat {α : Type u} {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} [semiring β] {hp : decidable_pred p} :
∑ (x : α) in s, ite (p x) 1 0 = ((finset.filter p s).card)

theorem finset.sum_nat_cast {α : Type u} {β : Type v} [add_comm_monoid β] [has_one β] (s : finset α) (f : α → ) :
∑ (x : α) in s, f x = ∑ (x : α) in s, (f x)

theorem finset.sum_int_cast {α : Type u} {β : Type v} [add_comm_group β] [has_one β] (s : finset α) (f : α → ) :
∑ (x : α) in s, f x = ∑ (x : α) in s, (f x)

theorem finset.sum_comp {α : Type u} {β : Type v} {γ : Type w} [add_comm_monoid β] [decidable_eq γ] {s : finset α} (f : γ → β) (g : α → γ) :
∑ (a : α) in s, f (g a) = ∑ (b : γ) in finset.image g s, (finset.filter (λ (a : α), g a = b) s).card •ℕ f b

theorem finset.sum_range_succ' {β : Type v} [add_comm_monoid β] (f : → β) (n : ) :
∑ (i : ) in finset.range (n + 1), f i = ∑ (i : ) in finset.range n, f (i + 1) + f 0

theorem finset.sum_flip {β : Type v} [add_comm_monoid β] {n : } (f : → β) :
∑ (i : ) in finset.range (n + 1), f (n - i) = ∑ (i : ) in finset.range (n + 1), f i

@[simp]
theorem finset.op_sum {α : Type u} {β : Type v} [add_comm_monoid β] {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} [add_comm_monoid β] {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 : α → β} [add_comm_group β] :
∑ (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 u} {σ : α → Type u_1} (s : finset α) (t : Π (a : α), finset (σ a)) :
(s.sigma t).card = ∑ (a : α) in s, (t a).card

theorem finset.card_bind {α : Type u} {β : Type v} [decidable_eq β] {s : finset α} {t : α → finset β} (h : ∀ (x : α), x s∀ (y : α), y sx ydisjoint (t x) (t y)) :
(s.bind t).card = ∑ (u : α) in s, (t u).card

theorem finset.card_bind_le {α : Type u} {β : Type v} [decidable_eq β] {s : finset α} {t : α → finset β} :
(s.bind 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 finset.image f s, (finset.filter (λ (x : α), f x = a) s).card

theorem finset.gsmul_sum {α : Type u} {β : Type v} [add_comm_group β] {f : α → β} {s : finset α} (z : ) :
z •ℤ ∑ (a : α) in s, f a = ∑ (a : α) in s, z •ℤ f a

@[simp]
theorem finset.sum_sub_distrib {α : Type u} {β : Type v} {s : finset α} {f g : α → β} [add_comm_group β] :
∑ (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 : α → β} [comm_monoid_with_zero β] (ha : a s) (h : f a = 0) :
∏ (x : α) in s, f x = 0

theorem finset.prod_boole {α : Type u} {β : Type v} [comm_monoid_with_zero β] {s : finset α} {p : α → Prop} [decidable_pred p] :
∏ (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 : α → β} [comm_monoid_with_zero β] [nontrivial β] [no_zero_divisors β] :
∏ (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 : α → β} [comm_monoid_with_zero β] [nontrivial β] [no_zero_divisors β] :
∏ (x : α) in s, f x 0 ∀ (a : α), a sf a 0

@[simp]
theorem finset.prod_inv_distrib' {α : Type u} {β : Type v} {s : finset α} {f : α → β} [comm_group_with_zero β] :
∏ (x : α) in s, (f x)⁻¹ = (∏ (x : α) in s, f x)⁻¹

theorem list.sum_to_finset {α : Type u} {M : Type u_1} [decidable_eq α] [add_comm_monoid M] (f : α → M) {l : list α} (hl : l.nodup) :

theorem list.prod_to_finset {α : Type u} {M : Type u_1} [decidable_eq α] [comm_monoid M] (f : α → M) {l : list α} (hl : l.nodup) :

@[simp]
theorem multiset.to_finset_sum_count_eq {α : Type u} [decidable_eq α] (s : multiset α) :
∑ (a : α) in s.to_finset, multiset.count a s = multiset.card s

theorem multiset.count_sum' {α : Type u} {β : Type v} [decidable_eq α] {s : finset β} {a : α} {f : β → multiset α} :
multiset.count a (∑ (x : β) in s, f x) = ∑ (x : β) in s, multiset.count a (f x)

@[simp]
theorem multiset.to_finset_sum_count_smul_eq {α : Type u} [decidable_eq α] (s : multiset α) :
∑ (a : α) in s.to_finset, multiset.count a s •ℕ (a ::ₘ 0) = s

theorem multiset.exists_smul_of_dvd_count {α : Type u} [decidable_eq α] (s : multiset α) {k : } (h : ∀ (a : α), k multiset.count a s) :
∃ (u : multiset α), s = k •ℕ u

@[simp]
theorem nat.coe_prod {α : Type u} {R : Type u_1} [comm_semiring R] (f : α → ) (s : finset α) :
∏ (i : α) in s, f i = ∏ (i : α) in s, (f i)

@[simp]
theorem int.coe_prod {α : Type u} {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 u} {M : Type u_1} [comm_monoid M] (f : α → units M) (s : finset α) :
∏ (i : α) in s, f i = ∏ (i : α) in s, (f i)