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 β] :
finset α(α → β) → β

∑ 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 β] :
finset α(α → β) → β

∏ 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 α] :
(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 α] :
(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 α] :
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 α] :
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 : α} :
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 : α} :
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 β] :
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 β] :
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 α] :
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 α] :
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 α] :
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 α] :
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

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 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⟩

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⟩

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 : γ → β) :
(∀ (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 : γ → β) :
(∀ (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 α} :
r 0 0(∀ (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 α} :
r 1 1(∀ (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 β] :
s₁ s₂(∀ (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 β] :
s₁ s₂(∀ (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] :
(∀ (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] :
(∀ (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 : α) :
(∀ (b : α), b sb af b = 0)(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 : α) :
(∀ (b : α), b sb af b = 1)(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] :
(∀ (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] :
(∀ (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 : α → β} :
(∀ (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 : α → β} :
(∀ (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 α} :
(∀ (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 α} :
(∀ (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_bij {α : Type u} {β : Type v} {γ : Type w} [add_comm_monoid β] {s : finset α} {t : finset γ} {f : α → β} {g : γ → β} (i : Π (a : α), a s → γ) :
(∀ (a : α) (ha : a s), i a ha t)(∀ (a : α) (ha : a s), f a = g (i a ha))(∀ (a₁ a₂ : α) (ha₁ : a₁ s) (ha₂ : a₂ s), i a₁ ha₁ = i a₂ ha₂a₁ = a₂)(∀ (b : γ), b t(∃ (a : α) (ha : a s), b = i a ha))∑ (x : α) in s, f x = ∑ (x : γ) in t, g x

theorem finset.prod_bij {α : Type u} {β : Type v} {γ : Type w} [comm_monoid β] {s : finset α} {t : finset γ} {f : α → β} {g : γ → β} (i : Π (a : α), a s → γ) :
(∀ (a : α) (ha : a s), i a ha t)(∀ (a : α) (ha : a s), f a = g (i a ha))(∀ (a₁ a₂ : α) (ha₁ : a₁ s) (ha₂ : a₂ s), i a₁ ha₁ = i a₂ ha₂a₁ = a₂)(∀ (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) :
(∀ (a : α) (ha : a s), j (i a ha) _ = a)(∀ (a : γ) (ha : a t), i (j a ha) _ = a)∑ (x : α) in s, f x = ∑ (x : γ) in t, g x

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) :
(∀ (a : α) (ha : a s), j (i a ha) _ = a)(∀ (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 → γ) :
(∀ (a : α) (h₁ : a s) (h₂ : f a 1), i a h₁ h₂ t)(∀ (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₂)(∀ (b : γ), b tg b 1(∃ (a : α) (h₁ : a s) (h₂ : f a 1), b = i a 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 → γ) :
(∀ (a : α) (h₁ : a s) (h₂ : f a 0), i a h₁ h₂ t)(∀ (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₂)(∀ (b : γ), b tg b 0(∃ (a : α) (h₁ : a s) (h₂ : f a 0), b = i a 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 β] :
∑ (x : α) in s, f x 0 → s.nonempty

theorem finset.nonempty_of_prod_ne_one {α : Type u} {β : Type v} {s : finset α} {f : α → β} [comm_monoid β] :
∏ (x : α) in s, f x 1 → s.nonempty

theorem finset.exists_ne_zero_of_sum_ne_zero {α : Type u} {β : Type v} {s : finset α} {f : α → β} [add_comm_monoid β] :
∑ (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 β] :
∏ (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 α] :
s₁ s₂(∀ (x : α), x s₂ \ s₁g x = 0)(∀ (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 α] :
s₁ s₂(∀ (x : α), x s₂ \ s₁g x = 1)(∀ (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) :
(∀ (a b : M), p ap bp (a * b))p 1(∀ (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) :
(∀ (a b : M), p ap bp (a + b))p 0(∀ (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) (h₂ : ∀ (a : α) (ha : a s), f a 1g a ha a) (h₃ : ∀ (a : α) (ha : a s), g a ha s) :
(∀ (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) (h₂ : ∀ (a : α) (ha : a s), f a 0g a ha a) (h₃ : ∀ (a : α) (ha : a s), g a ha s) :
(∀ (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.prod_cancels_of_partition_cancels {α : Type u} {β : Type v} {s : finset α} {f : α → β} [comm_monoid β] (R : setoid α) [decidable_rel setoid.r] :
(∀ (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] :
(∀ (x : α), x s∑ (a : α) in finset.filter (λ (y : α), y x) s, f a = 0)∑ (x : α) in s, f x = 0

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 : α) :
x sf 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 : α) :
x sf 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 : α} :
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 : α} :
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 : α) :
x sf 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 : α) :
x sf 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 : α → β} :
i sg i + h i = f i(∀ (j : α), j sj ig j = f j)(∀ (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 : α → } :
(∀ (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_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.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 β} :
(∀ (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 β} :
(∀ (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 β] :
a sf 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 α} :
l.nodupl.to_finset.sum f = (list.map f l).sum

theorem list.prod_to_finset {α : Type u} {M : Type u_1} [decidable_eq α] [comm_monoid M] (f : α → M) {l : list α} :
l.nodupl.to_finset.prod f = (list.map f l).prod

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

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)

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 : } :
(∀ (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)