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.

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} [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
@[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} [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 u} {γ : Type w} [semiring β] [semiring γ] (f : β →+* γ) (l : list β) :
theorem ring_hom.map_list_sum {β : Type u} {γ : Type w} [non_assoc_semiring β] [non_assoc_semiring γ] (f : β →+* γ) (l : list β) :
theorem ring_hom.map_multiset_prod {β : Type u} {γ : Type w} [comm_semiring β] [comm_semiring γ] (f : β →+* γ) (s : multiset β) :
theorem ring_hom.map_multiset_sum {β : Type u} {γ : Type w} [non_assoc_semiring β] [non_assoc_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} [non_assoc_semiring β] [non_assoc_semiring γ] (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} [add_zero_class β] [add_comm_monoid γ] (f : α → β →+ γ) (s : finset α) :
∑ (x : α) in s, f x = ∑ (x : α) in s, (f x)
theorem monoid_hom.coe_prod {β : Type u} {α : Type v} {γ : Type w} [mul_one_class β] [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} [add_zero_class β] [add_comm_monoid γ] (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} [mul_one_class β] [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} [add_comm_monoid β] {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 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 v} {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 is_compl.sum_add_sum {β : Type u} {α : Type v} [fintype α] [decidable_eq α] [add_comm_monoid β] {s t : finset α} (h : is_compl s 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 : is_compl s 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} [add_comm_monoid β] [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} [add_comm_monoid β] [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 : α → β} [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.map function.embedding.inl s finset.map function.embedding.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.map function.embedding.inl s finset.map function.embedding.inr t, sum.elim f 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 : γ → finset α} :
(∀ (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 : α → β} [add_comm_monoid β] [decidable_eq α] {s : finset γ} {t : γ → finset α} :
(∀ (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} [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.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} [add_comm_monoid β] {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} [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_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} [add_comm_monoid β] {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} [add_comm_monoid β] {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 α} [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.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} [add_comm_monoid β] (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} [add_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_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.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 α} [add_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.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 α} [add_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_apply_ite_of_false {β : Type u} {α : Type v} {γ : Type w} {s : finset α} [add_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.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 α} [add_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.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} [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)
@[simp]
theorem finset.sum_dite_irrel {β : Type u} {α : Type v} [add_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.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 ι] [add_comm_monoid M] (i : ι) (x : M) (s : finset ι) :
∑ (j : ι) in s, pi.single i 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, pi.single j (f j) i = ite (i s) (f i) 0
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.prod_range_succ_comm {β : Type u} [comm_monoid β] (f : → β) (n : ) :
∏ (x : ) in finset.range (n + 1), f x = (f n) * ∏ (x : ) in finset.range n, f x
theorem finset.sum_range_succ_comm {β : Type u} [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 u} [comm_monoid β] (f : → β) (n : ) :
∏ (x : ) in finset.range (n + 1), f x = (∏ (x : ) in finset.range n, f x) * f n
theorem finset.sum_range_succ {β : Type u} [add_comm_monoid β] (f : → β) (n : ) :
∑ (x : ) in finset.range (n + 1), f x = ∑ (x : ) in finset.range n, 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 finset.range n, f (k + 1)) * f 0
theorem finset.sum_range_succ' {β : Type u} [add_comm_monoid β] (f : → β) (n : ) :
∑ (k : ) in finset.range (n + 1), f k = ∑ (k : ) in finset.range n, f (k + 1) + f 0
theorem finset.eventually_constant_sum {β : Type u} [add_comm_monoid β] {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 finset.range n, f x) * ∏ (x : ) in finset.range m, f (n + x)
theorem finset.sum_range_add {β : Type u} [add_comm_monoid β] (f : → β) (n m : ) :
∑ (x : ) in finset.range (n + m), f x = ∑ (x : ) in finset.range n, f x + ∑ (x : ) in finset.range m, f (n + x)
theorem finset.sum_range_zero {β : Type u} [add_comm_monoid β] (f : → β) :
∑ (k : ) in finset.range 0, f k = 0
theorem finset.prod_range_zero {β : Type u} [comm_monoid β] (f : → β) :
∏ (k : ) in finset.range 0, f k = 1
theorem finset.sum_range_one {β : Type u} [add_comm_monoid β] (f : → β) :
∑ (k : ) in finset.range 1, f k = f 0
theorem finset.prod_range_one {β : Type u} [comm_monoid β] (f : → β) :
∏ (k : ) in finset.range 1, 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) :
(multiset.map f s).prod = ∏ (m : α) in s.to_finset, f m ^ multiset.count m s
theorem finset.sum_multiset_map_count {α : Type v} [decidable_eq α] (s : multiset α) {M : Type u_1} [add_comm_monoid M] (f : α → M) :
(multiset.map f s).sum = ∑ (m : α) in s.to_finset, multiset.count m s f m
theorem finset.sum_multiset_count {α : Type v} [decidable_eq α] [add_comm_monoid α] (s : multiset α) :
s.sum = ∑ (m : α) in s.to_finset, multiset.count m s m
theorem finset.prod_multiset_count {α : Type v} [decidable_eq α] [comm_monoid α] (s : multiset α) :
s.prod = ∏ (m : α) in s.to_finset, m ^ multiset.count m s
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} [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.sum_induction_nonempty {α : Type v} {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)) (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 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 u} [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 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} [add_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.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} [add_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.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} [add_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 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} [add_comm_monoid β] [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} [add_comm_monoid β] [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 : α → β} [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_sum_eq {β : Type u} {α : Type v} [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.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} [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 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} [non_assoc_semiring β] {hp : decidable_pred p} :
∑ (x : α) in s, ite (p x) 1 0 = ((finset.filter p s).card)
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.eq_sum_range_sub {β : Type u} [add_comm_group β] (f : → β) (n : ) :
f n = f 0 + ∑ (i : ) in finset.range n, (f (i + 1) - f i)
theorem finset.eq_sum_range_sub' {β : Type u} [add_comm_group β] (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} [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 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 : α → finset β} (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 : α → finset β} :
(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 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 : ) :
gsmul z (∑ (a : α) in s, f a) = ∑ (a : α) in s, gsmul 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 fintype.sum_bijective {α : Type u_1} {β : Type u_2} {M : Type u_3} [fintype α] [fintype β] [add_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.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 β] [add_comm_monoid M] (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 : α → β} [add_comm_monoid β] :
∑ (i : s), f i = ∑ (i : α) in s, f i
theorem list.sum_to_finset {α : Type v} {M : Type u_1} [decidable_eq α] [add_comm_monoid M] (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) :
@[simp]
theorem multiset.to_finset_sum_count_eq {α : Type v} [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_nsmul_eq {α : Type v} [decidable_eq α] (s : multiset α) :
∑ (a : α) in s.to_finset, multiset.count a s (a ::ₘ 0) = s
theorem multiset.exists_smul_of_dvd_count {α : Type v} [decidable_eq α] (s : multiset α) {k : } (h : ∀ (a : α), k multiset.count a s) :
∃ (u : multiset α), s = k u
@[simp]
theorem nat.cast_sum {β : Type u} {α : Type v} [add_comm_monoid β] [has_one β] (s : finset α) (f : α → ) :
∑ (x : α) in s, f x = ∑ (x : α) in s, (f x)
@[simp]
theorem int.cast_sum {β : Type u} {α : Type v} [add_comm_group β] [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} [comm_semiring R] (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 : α → units M) (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