# Big operators #

In this file we prove theorems about products and sums indexed by a `Finset`.

source
theorem Finset.prod_eq_fold {ι : Type u_1} {M : Type u_4} [CommMonoid M] (s : Finset ι) (f : ι → M) :
∏ i ∈ s, f i = fold (fun (x1 x2 : M) => x1 * x2) 1 f s
source
theorem Finset.sum_eq_fold {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (f : ι → M) :
∑ i ∈ s, f i = fold (fun (x1 x2 : M) => x1 + x2) 0 f s
source
@[simp]
theorem Finset.prod_cons {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [CommMonoid M] {f : ι → M} (h : a ∉ s) :
∏ x ∈ cons a s h, f x = f a * ∏ x ∈ s, f x
source
@[simp]
theorem Finset.sum_cons {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [AddCommMonoid M] {f : ι → M} (h : a ∉ s) :
∑ x ∈ cons a s h, f x = f a + ∑ x ∈ s, f x
source
theorem Finset.prod_cons' {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [CommMonoid M] (h : a ∉ s) :
(cons a s h).prod = fun (f : ι → M) => f a * ∏ x ∈ s, f x

Variant of `prod_cons` not applied to a function.

source
theorem Finset.sum_cons' {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [AddCommMonoid M] (h : a ∉ s) :
(cons a s h).sum = fun (f : ι → M) => f a + ∑ x ∈ s, f x
source
@[simp]
theorem Finset.prod_insert {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [CommMonoid M] {f : ι → M} [DecidableEq ι] :
a ∉ s → ∏ x ∈ insert a s, f x = f a * ∏ x ∈ s, f x
source
@[simp]
theorem Finset.sum_insert {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] :
a ∉ s → ∑ x ∈ insert a s, f x = f a + ∑ x ∈ s, f x
source
theorem Finset.prod_insert' {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [CommMonoid M] [DecidableEq ι] (h : a ∉ s) :
(insert a s).prod = fun (f : ι → M) => f a * ∏ x ∈ s, f x

Variant of `prod_insert` not applied to a function.

source
theorem Finset.sum_insert' {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [AddCommMonoid M] [DecidableEq ι] (h : a ∉ s) :
(insert a s).sum = fun (f : ι → M) => f a + ∑ x ∈ s, f x
source
@[simp]
theorem Finset.prod_insert_of_eq_one_if_notMem {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [CommMonoid M] {f : ι → M} [DecidableEq ι] (h : a ∉ s → f a = 1) :
∏ x ∈ insert a s, f x = ∏ x ∈ 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`.

source
@[simp]
theorem Finset.sum_insert_of_eq_zero_if_notMem {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] (h : a ∉ s → f a = 0) :
∑ x ∈ insert a s, f x = ∑ x ∈ 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`.

source
@[deprecated Finset.sum_insert_of_eq_zero_if_notMem (since := "2025-05-23")]
theorem Finset.sum_insert_of_eq_zero_if_not_mem {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] (h : a ∉ s → f a = 0) :
∑ x ∈ insert a s, f x = ∑ x ∈ s, f x

Alias of `Finset.sum_insert_of_eq_zero_if_notMem`.

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

source
@[deprecated Finset.prod_insert_of_eq_one_if_notMem (since := "2025-05-23")]
theorem Finset.prod_insert_of_eq_one_if_not_mem {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [CommMonoid M] {f : ι → M} [DecidableEq ι] (h : a ∉ s → f a = 1) :
∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

Alias of `Finset.prod_insert_of_eq_one_if_notMem`.

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

source
theorem Finset.prod_insert_one {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [CommMonoid M] {f : ι → M} [DecidableEq ι] (h : f a = 1) :
∏ x ∈ insert a s, f x = ∏ x ∈ 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`.

source
theorem Finset.sum_insert_zero {ι : Type u_1} {M : Type u_4} {s : Finset ι} {a : ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] (h : f a = 0) :
∑ x ∈ insert a s, f x = ∑ x ∈ 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`.

source
@[simp]
theorem Finset.prod_singleton {ι : Type u_1} {M : Type u_4} [CommMonoid M] (f : ι → M) (a : ι) :
∏ x ∈ {a}, f x = f a
source
@[simp]
theorem Finset.sum_singleton {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (f : ι → M) (a : ι) :
∑ x ∈ {a}, f x = f a
source
theorem Finset.prod_singleton' {ι : Type u_1} {M : Type u_4} [CommMonoid M] (a : ι) :
{a}.prod = fun (f : ι → M) => f a

Variant of `prod_singleton` not applied to a function.

source
theorem Finset.sum_singleton' {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (a : ι) :
{a}.sum = fun (f : ι → M) => f a
source
theorem Finset.prod_pair {ι : Type u_1} {M : Type u_4} [CommMonoid M] {f : ι → M} [DecidableEq ι] {a b : ι} (h : a ≠ b) :
∏ x ∈ {a, b}, f x = f a * f b
source
theorem Finset.sum_pair {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] {a b : ι} (h : a ≠ b) :
∑ x ∈ {a, b}, f x = f a + f b
source
@[simp]
theorem Finset.prod_image {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] {f : ι → M} [DecidableEq ι] {s : Finset κ} {g : κ → ι} :
Set.InjOn g ↑s → ∏ x ∈ image g s, f x = ∏ x ∈ s, f (g x)
source
@[simp]
theorem Finset.sum_image {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] {s : Finset κ} {g : κ → ι} :
Set.InjOn g ↑s → ∑ x ∈ image g s, f x = ∑ x ∈ s, f (g x)
source
theorem Finset.prod_attach {ι : Type u_1} {M : Type u_4} [CommMonoid M] (s : Finset ι) (f : ι → M) :
∏ x ∈ s.attach, f ↑x = ∏ x ∈ s, f x
source
theorem Finset.sum_attach {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (f : ι → M) :
∑ x ∈ s.attach, f ↑x = ∑ x ∈ s, f x
source
theorem Finset.prod_congr {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [CommMonoid M] {f g : ι → M} (h : s₁ = s₂) :
(∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g
source
theorem Finset.sum_congr {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f g : ι → M} (h : s₁ = s₂) :
(∀ x ∈ s₂, f x = g x) → s₁.sum f = s₂.sum g
source
theorem Finset.prod_eq_one {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : ι → M} (h : ∀ x ∈ s, f x = 1) :
∏ x ∈ s, f x = 1
source
theorem Finset.sum_eq_zero {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (h : ∀ x ∈ s, f x = 0) :
∑ x ∈ s, f x = 0
source
@[simp]
theorem Finset.prod_eq_one_iff {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : ι → M} [Subsingleton M ˣ] :
∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1

In a monoid whose only unit is `1`, a product is equal to `1` iff all factors are `1`.

source
@[simp]
theorem Finset.sum_eq_zero_iff {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} [Subsingleton (AddUnits M)] :
∑ i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0

In an additive monoid whose only unit is `0`, a sum is equal to `0` iff all terms are `0`.

source
theorem Finset.prod_disjUnion {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [CommMonoid M] {f : ι → M} (h : Disjoint s₁ s₂) :
∏ x ∈ s₁.disjUnion s₂ h, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x
source
theorem Finset.sum_disjUnion {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f : ι → M} (h : Disjoint s₁ s₂) :
∑ x ∈ s₁.disjUnion s₂ h, f x = ∑ x ∈ s₁, f x + ∑ x ∈ s₂, f x
source
theorem Finset.prod_disjiUnion {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] {f : ι → M} (s : Finset κ) (t : κ → Finset ι) (h : (↑s).PairwiseDisjoint t) :
∏ x ∈ s.disjiUnion t h, f x = ∏ i ∈ s, ∏ x ∈ t i, f x
source
theorem Finset.sum_disjiUnion {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {f : ι → M} (s : Finset κ) (t : κ → Finset ι) (h : (↑s).PairwiseDisjoint t) :
∑ x ∈ s.disjiUnion t h, f x = ∑ i ∈ s, ∑ x ∈ t i, f x
source
theorem Finset.prod_union_inter {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [CommMonoid M] {f : ι → M} [DecidableEq ι] :
(∏ x ∈ s₁ ∪ s₂, f x) * ∏ x ∈ s₁ ∩ s₂, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x
source
theorem Finset.sum_union_inter {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] :
∑ x ∈ s₁ ∪ s₂, f x + ∑ x ∈ s₁ ∩ s₂, f x = ∑ x ∈ s₁, f x + ∑ x ∈ s₂, f x
source
theorem Finset.prod_union {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [CommMonoid M] {f : ι → M} [DecidableEq ι] (h : Disjoint s₁ s₂) :
∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x
source
theorem Finset.sum_union {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] (h : Disjoint s₁ s₂) :
∑ x ∈ s₁ ∪ s₂, f x = ∑ x ∈ s₁, f x + ∑ x ∈ s₂, f x
source
theorem Finset.prod_filter_mul_prod_filter_not {ι : Type u_1} {M : Type u_4} [CommMonoid M] (s : Finset ι) (p : ι → Prop) [DecidablePred p] [(x : ι) → Decidable ¬p x] (f : ι → M) :
(∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, f x = ∏ x ∈ s, f x
source
theorem Finset.sum_filter_add_sum_filter_not {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (p : ι → Prop) [DecidablePred p] [(x : ι) → Decidable ¬p x] (f : ι → M) :
∑ x ∈ s with p x, f x + ∑ x ∈ s with ¬p x, f x = ∑ x ∈ s, f x
source
theorem Finset.prod_filter_not_mul_prod_filter {ι : Type u_1} {M : Type u_4} [CommMonoid M] (s : Finset ι) (p : ι → Prop) [DecidablePred p] [(x : ι) → Decidable ¬p x] (f : ι → M) :
(∏ x ∈ s with ¬p x, f x) * ∏ x ∈ s with p x, f x = ∏ x ∈ s, f x
source
theorem Finset.sum_filter_not_add_sum_filter {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (p : ι → Prop) [DecidablePred p] [(x : ι) → Decidable ¬p x] (f : ι → M) :
∑ x ∈ s with ¬p x, f x + ∑ x ∈ s with p x, f x = ∑ x ∈ s, f x
source
theorem Finset.prod_filter_xor {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : ι → M} (p q : ι → Prop) [DecidablePred p] [DecidablePred q] :
∏ x ∈ s with Xor' (p x) (q x), f x = (∏ x ∈ s with p x ∧ ¬q x, f x) * ∏ x ∈ s with q x ∧ ¬p x, f x
source
theorem Finset.sum_filter_xor {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (p q : ι → Prop) [DecidablePred p] [DecidablePred q] :
∑ x ∈ s with Xor' (p x) (q x), f x = ∑ x ∈ s with p x ∧ ¬q x, f x + ∑ x ∈ s with q x ∧ ¬p x, f x
source
theorem IsCompl.prod_mul_prod {ι : Type u_1} {M : Type u_4} [CommMonoid M] [Fintype ι] {s t : Finset ι} (h : IsCompl s t) (f : ι → M) :
(∏ i ∈ s, f i) * ∏ i ∈ t, f i = ∏ i : ι, f i
source
theorem IsCompl.sum_add_sum {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Fintype ι] {s t : Finset ι} (h : IsCompl s t) (f : ι → M) :
∑ i ∈ s, f i + ∑ i ∈ t, f i = ∑ i : ι, f i
source
theorem Finset.prod_mul_prod_compl {ι : Type u_1} {M : Type u_4} [CommMonoid M] [Fintype ι] [DecidableEq ι] (s : Finset ι) (f : ι → M) :
(∏ i ∈ s, f i) * ∏ i ∈ s ᶜ, f i = ∏ i : ι, f i

Multiplying the products of a function over `s` and over `sᶜ` gives the whole product. For a version expressed with subtypes, see `Fintype.prod_subtype_mul_prod_subtype`.

source
theorem Finset.sum_add_sum_compl {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Fintype ι] [DecidableEq ι] (s : Finset ι) (f : ι → M) :
∑ i ∈ s, f i + ∑ i ∈ s ᶜ, f i = ∑ i : ι, f i

Adding the sums of a function over `s` and over `sᶜ` gives the whole sum. For a version expressed with subtypes, see `Fintype.sum_subtype_add_sum_subtype`.

source
theorem Finset.prod_compl_mul_prod {ι : Type u_1} {M : Type u_4} [CommMonoid M] [Fintype ι] [DecidableEq ι] (s : Finset ι) (f : ι → M) :
(∏ i ∈ s ᶜ, f i) * ∏ i ∈ s, f i = ∏ i : ι, f i
source
theorem Finset.sum_compl_add_sum {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Fintype ι] [DecidableEq ι] (s : Finset ι) (f : ι → M) :
∑ i ∈ s ᶜ, f i + ∑ i ∈ s, f i = ∑ i : ι, f i
source
theorem Finset.prod_sdiff {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [CommMonoid M] {f : ι → M} [DecidableEq ι] (h : s₁ ⊆ s₂) :
(∏ x ∈ s₂ \ s₁, f x) * ∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x
source
theorem Finset.sum_sdiff {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] (h : s₁ ⊆ s₂) :
∑ x ∈ s₂ \ s₁, f x + ∑ x ∈ s₁, f x = ∑ x ∈ s₂, f x
source
theorem Finset.prod_subset_one_on_sdiff {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [CommMonoid M] {f g : ι → M} [DecidableEq ι] (h : s₁ ⊆ s₂) (hg : ∀ x ∈ s₂ \ s₁, g x = 1) (hfg : ∀ x ∈ s₁, f x = g x) :
∏ i ∈ s₁, f i = ∏ i ∈ s₂, g i
source
theorem Finset.sum_subset_zero_on_sdiff {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f g : ι → M} [DecidableEq ι] (h : s₁ ⊆ s₂) (hg : ∀ x ∈ s₂ \ s₁, g x = 0) (hfg : ∀ x ∈ s₁, f x = g x) :
∑ i ∈ s₁, f i = ∑ i ∈ s₂, g i
source
theorem Finset.prod_subset {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [CommMonoid M] {f : ι → M} (h : s₁ ⊆ s₂) (hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 1) :
∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x
source
theorem Finset.sum_subset {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f : ι → M} (h : s₁ ⊆ s₂) (hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 0) :
∑ x ∈ s₁, f x = ∑ x ∈ s₂, f x
source
@[simp]
theorem Finset.prod_disjSum {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] (s : Finset ι) (t : Finset κ) (f : ι ⊕ κ → M) :
∏ x ∈ s.disjSum t, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)
source
@[simp]
theorem Finset.sum_disjSum {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (t : Finset κ) (f : ι ⊕ κ → M) :
∑ x ∈ s.disjSum t, f x = ∑ x ∈ s, f (Sum.inl x) + ∑ x ∈ t, f (Sum.inr x)
source
@[deprecated Finset.sum_disjSum (since := "2025-06-11")]
theorem Finset.sum_disj_sum {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (t : Finset κ) (f : ι ⊕ κ → M) :
∑ x ∈ s.disjSum t, f x = ∑ x ∈ s, f (Sum.inl x) + ∑ x ∈ t, f (Sum.inr x)

Alias of `Finset.sum_disjSum`.

source
@[deprecated Finset.prod_disjSum (since := "2025-06-11")]
theorem Finset.prod_disj_sum {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] (s : Finset ι) (t : Finset κ) (f : ι ⊕ κ → M) :
∏ x ∈ s.disjSum t, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)

Alias of `Finset.prod_disjSum`.

source
theorem Finset.prod_sum_eq_prod_toLeft_mul_prod_toRight {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] (s : Finset (ι ⊕ κ)) (f : ι ⊕ κ → M) :
∏ x ∈ s, f x = (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x)
source
theorem Finset.sum_sum_eq_sum_toLeft_add_sum_toRight {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] (s : Finset (ι ⊕ κ)) (f : ι ⊕ κ → M) :
∑ x ∈ s, f x = ∑ x ∈ s.toLeft, f (Sum.inl x) + ∑ x ∈ s.toRight, f (Sum.inr x)
source
theorem Finset.prod_sumElim {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] (s : Finset ι) (t : Finset κ) (f : ι → M) (g : κ → M) :
∏ x ∈ s.disjSum t, Sum.elim f g x = (∏ x ∈ s, f x) * ∏ x ∈ t, g x
source
theorem Finset.sum_sumElim {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (t : Finset κ) (f : ι → M) (g : κ → M) :
∑ x ∈ s.disjSum t, Sum.elim f g x = ∑ x ∈ s, f x + ∑ x ∈ t, g x
source
theorem Finset.prod_biUnion {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] {f : ι → M} [DecidableEq ι] {s : Finset κ} {t : κ → Finset ι} (hs : (↑s).PairwiseDisjoint t) :
∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i
source
theorem Finset.sum_biUnion {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] {s : Finset κ} {t : κ → Finset ι} (hs : (↑s).PairwiseDisjoint t) :
∑ x ∈ s.biUnion t, f x = ∑ x ∈ s, ∑ i ∈ t x, f i
source
theorem Finset.prod_of_injOn {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (e : ι → κ) (he : Set.InjOn e ↑s) (hest : Set.MapsTo e ↑s ↑t) (h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1) (h : ∀ i ∈ s, f i = g (e i)) :
∏ i ∈ s, f i = ∏ j ∈ t, g j
source
theorem Finset.sum_of_injOn {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (e : ι → κ) (he : Set.InjOn e ↑s) (hest : Set.MapsTo e ↑s ↑t) (h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 0) (h : ∀ i ∈ s, f i = g (e i)) :
∑ i ∈ s, f i = ∑ j ∈ t, g j
source
theorem Finset.prod_fiberwise_eq_prod_filter {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : ι → M) :
∏ j ∈ t, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s with g i ∈ t, f i
source
theorem Finset.sum_fiberwise_eq_sum_filter {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : ι → M) :
∑ j ∈ t, ∑ i ∈ s with g i = j, f i = ∑ i ∈ s with g i ∈ t, f i
source
theorem Finset.prod_fiberwise_eq_prod_filter' {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : κ → M) :
∏ j ∈ t, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s with g i ∈ t, f (g i)
source
theorem Finset.sum_fiberwise_eq_sum_filter' {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : κ → M) :
∑ j ∈ t, ∑ i ∈ s with g i = j, f j = ∑ i ∈ s with g i ∈ t, f (g i)
source
theorem Finset.prod_fiberwise_of_maps_to {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : ι → M) :
∏ j ∈ t, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s, f i
source
theorem Finset.sum_fiberwise_of_maps_to {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : ι → M) :
∑ j ∈ t, ∑ i ∈ s with g i = j, f i = ∑ i ∈ s, f i
source
theorem Finset.prod_fiberwise_of_maps_to' {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : κ → M) :
∏ j ∈ t, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s, f (g i)
source
theorem Finset.sum_fiberwise_of_maps_to' {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : κ → M) :
∑ j ∈ t, ∑ i ∈ s with g i = j, f j = ∑ i ∈ s, f (g i)
source
theorem Finset.prod_fiberwise {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : ι → M) :
∏ j : κ, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s, f i
source
theorem Finset.sum_fiberwise {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : ι → M) :
∑ j : κ, ∑ i ∈ s with g i = j, f i = ∑ i ∈ s, f i
source
theorem Finset.prod_fiberwise' {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : κ → M) :
∏ j : κ, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s, f (g i)
source
theorem Finset.sum_fiberwise' {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : κ → M) :
∑ j : κ, ∑ i ∈ s with g i = j, f j = ∑ i ∈ s, f (g i)
source
@[simp]
theorem Finset.prod_diag {ι : Type u_1} {M : Type u_4} [CommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι × ι → M) :
∏ i ∈ s.diag, f i = ∏ i ∈ s, f (i, i)
source
@[simp]
theorem Finset.sum_diag {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι × ι → M) :
∑ i ∈ s.diag, f i = ∑ i ∈ s, f (i, i)
source
theorem Finset.prod_image' {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] {f : ι → M} [DecidableEq ι] {s : Finset κ} {g : κ → ι} (h : κ → M) (eq : ∀ i ∈ s, f (g i) = ∏ j ∈ s with g j = g i, h j) :
∏ a ∈ image g s, f a = ∏ i ∈ s, h i
source
theorem Finset.sum_image' {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] {s : Finset κ} {g : κ → ι} (h : κ → M) (eq : ∀ i ∈ s, f (g i) = ∑ j ∈ s with g j = g i, h j) :
∑ a ∈ image g s, f a = ∑ i ∈ s, h i
source
theorem Finset.prod_mul_distrib {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f g : ι → M} :
∏ x ∈ s, f x * g x = (∏ x ∈ s, f x) * ∏ x ∈ s, g x
source
theorem Finset.sum_add_distrib {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f g : ι → M} :
∑ x ∈ s, (f x + g x) = ∑ x ∈ s, f x + ∑ x ∈ s, g x
source
theorem Finset.prod_mul_prod_comm {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] (f g h i : ι → M) :
(∏ a ∈ s, f a * g a) * ∏ a ∈ s, h a * i a = (∏ a ∈ s, f a * h a) * ∏ a ∈ s, g a * i a
source
theorem Finset.sum_add_sum_comm {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] (f g h i : ι → M) :
∑ a ∈ s, (f a + g a) + ∑ a ∈ s, (h a + i a) = ∑ a ∈ s, (f a + h a) + ∑ a ∈ s, (g a + i a)
source
theorem Finset.prod_filter_of_ne {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : ι → M} {p : ι → Prop} [DecidablePred p] (hp : ∀ x ∈ s, f x ≠ 1 → p x) :
∏ x ∈ s with p x, f x = ∏ x ∈ s, f x
source
theorem Finset.sum_filter_of_ne {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} {p : ι → Prop} [DecidablePred p] (hp : ∀ x ∈ s, f x ≠ 0 → p x) :
∑ x ∈ s with p x, f x = ∑ x ∈ s, f x
source
theorem Finset.prod_filter_ne_one {ι : Type u_1} {M : Type u_4} [CommMonoid M] {f : ι → M} (s : Finset ι) [(x : ι) → Decidable (f x ≠ 1)] :
∏ x ∈ s with f x ≠ 1, f x = ∏ x ∈ s, f x
source
theorem Finset.sum_filter_ne_zero {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {f : ι → M} (s : Finset ι) [(x : ι) → Decidable (f x ≠ 0)] :
∑ x ∈ s with f x ≠ 0, f x = ∑ x ∈ s, f x
source
theorem Finset.prod_filter {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] (p : ι → Prop) [DecidablePred p] (f : ι → M) :
∏ a ∈ s with p a, f a = ∏ a ∈ s, if p a then f a else 1
source
theorem Finset.sum_filter {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] (p : ι → Prop) [DecidablePred p] (f : ι → M) :
∑ a ∈ s with p a, f a = ∑ a ∈ s, if p a then f a else 0
source
theorem Finset.prod_eq_single_of_mem {ι : Type u_1} {M : Type u_4} [CommMonoid M] {s : Finset ι} {f : ι → M} (a : ι) (h : a ∈ s) (h₀ : ∀ b ∈ s, b ≠ a → f b = 1) :
∏ x ∈ s, f x = f a
source
theorem Finset.sum_eq_single_of_mem {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {f : ι → M} (a : ι) (h : a ∈ s) (h₀ : ∀ b ∈ s, b ≠ a → f b = 0) :
∑ x ∈ s, f x = f a
source
theorem Finset.prod_eq_single {ι : Type u_1} {M : Type u_4} [CommMonoid M] {s : Finset ι} {f : ι → M} (a : ι) (h₀ : ∀ b ∈ s, b ≠ a → f b = 1) (h₁ : a ∉ s → f a = 1) :
∏ x ∈ s, f x = f a
source
theorem Finset.sum_eq_single {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {f : ι → M} (a : ι) (h₀ : ∀ b ∈ s, b ≠ a → f b = 0) (h₁ : a ∉ s → f a = 0) :
∑ x ∈ s, f x = f a
source
theorem Finset.prod_eq_ite {ι : Type u_1} {M : Type u_4} [CommMonoid M] [DecidableEq ι] {s : Finset ι} {f : ι → M} (a : ι) (h₀ : ∀ b ∈ s, b ≠ a → f b = 1) :
∏ x ∈ s, f x = if a ∈ s then f a else 1
source
theorem Finset.sum_eq_ite {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] {s : Finset ι} {f : ι → M} (a : ι) (h₀ : ∀ b ∈ s, b ≠ a → f b = 0) :
∑ x ∈ s, f x = if a ∈ s then f a else 0
source
theorem Finset.prod_union_eq_left {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [CommMonoid M] {f : ι → M} [DecidableEq ι] (hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 1) :
∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₁, f a
source
theorem Finset.sum_union_eq_left {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] (hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 0) :
∑ a ∈ s₁ ∪ s₂, f a = ∑ a ∈ s₁, f a
source
theorem Finset.prod_union_eq_right {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [CommMonoid M] {f : ι → M} [DecidableEq ι] (hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1) :
∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₂, f a
source
theorem Finset.sum_union_eq_right {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f : ι → M} [DecidableEq ι] (hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 0) :
∑ a ∈ s₁ ∪ s₂, f a = ∑ a ∈ s₂, f a
source
theorem Finset.prod_congr_of_eq_on_inter {ι : Type u_5} {M : Type u_6} {s₁ s₂ : Finset ι} {f g : ι → M} [CommMonoid M] (h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1) (h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1) (h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a) :
∏ a ∈ s₁, f a = ∏ a ∈ s₂, g a

The products of two functions `f g : ι → M` over finite sets `s₁ s₂ : Finset ι` are equal if the functions agree on `s₁ ∩ s₂`, `f = 1` and `g = 1` on the respective set differences.

source
theorem Finset.sum_congr_of_eq_on_inter {ι : Type u_5} {M : Type u_6} {s₁ s₂ : Finset ι} {f g : ι → M} [AddCommMonoid M] (h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 0) (h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 0) (h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a) :
∑ a ∈ s₁, f a = ∑ a ∈ s₂, g a

The sum of two functions `f g : ι → M` over finite sets `s₁ s₂ : Finset ι` are equal if the functions agree on `s₁ ∩ s₂`, `f = 0` and `g = 0` on the respective set differences.

source
theorem Finset.prod_eq_mul_of_mem {ι : Type u_1} {M : Type u_4} [CommMonoid M] {s : Finset ι} {f : ι → M} (a b : ι) (ha : a ∈ s) (hb : b ∈ s) (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) :
∏ x ∈ s, f x = f a * f b
source
theorem Finset.sum_eq_add_of_mem {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {f : ι → M} (a b : ι) (ha : a ∈ s) (hb : b ∈ s) (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 0) :
∑ x ∈ s, f x = f a + f b
source
theorem Finset.prod_eq_mul {ι : Type u_1} {M : Type u_4} [CommMonoid M] {s : Finset ι} {f : ι → M} (a b : ι) (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) (ha : a ∉ s → f a = 1) (hb : b ∉ s → f b = 1) :
∏ x ∈ s, f x = f a * f b
source
theorem Finset.sum_eq_add {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {f : ι → M} (a b : ι) (hn : a ≠ b) (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 0) (ha : a ∉ s → f a = 0) (hb : b ∉ s → f b = 0) :
∑ x ∈ s, f x = f a + f b
source
@[simp]
theorem Finset.prod_subtype_eq_prod_filter {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] (f : ι → M) {p : ι → Prop} [DecidablePred p] :
∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s with p x, f x

A product over `s.subtype p` equals one over `{x ∈ s | p x}`.

source
@[simp]
theorem Finset.sum_subtype_eq_sum_filter {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] (f : ι → M) {p : ι → Prop} [DecidablePred p] :
∑ x ∈ Finset.subtype p s, f ↑x = ∑ x ∈ s with p x, f x

A sum over `s.subtype p` equals one over `{x ∈ s | p x}`.

source
theorem Finset.prod_subtype_of_mem {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] (f : ι → M) {p : ι → Prop} [DecidablePred p] (h : ∀ x ∈ s, p x) :
∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s, f x

If all elements of a `Finset` satisfy the predicate `p`, a product over `s.subtype p` equals that product over `s`.

source
theorem Finset.sum_subtype_of_mem {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] (f : ι → M) {p : ι → Prop} [DecidablePred p] (h : ∀ x ∈ s, p x) :
∑ x ∈ Finset.subtype p s, f ↑x = ∑ x ∈ s, f x

If all elements of a `Finset` satisfy the predicate `p`, a sum over `s.subtype p` equals that sum over `s`.

source
theorem Finset.prod_subtype_map_embedding {ι : Type u_1} {M : Type u_4} [CommMonoid M] {p : ι → Prop} {s : Finset { x : ι // p x }} {f : { x : ι // p x } → M} {g : ι → M} (h : ∀ x ∈ s, g ↑x = f x) :
∏ x ∈ map (Function.Embedding.subtype fun (x : ι) => p x) s, g x = ∏ x ∈ 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`.

source
theorem Finset.sum_subtype_map_embedding {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {p : ι → Prop} {s : Finset { x : ι // p x }} {f : { x : ι // p x } → M} {g : ι → M} (h : ∀ x ∈ s, g ↑x = f x) :
∑ x ∈ map (Function.Embedding.subtype fun (x : ι) => p x) s, g x = ∑ x ∈ 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`.

source
theorem Finset.prod_coe_sort {ι : Type u_1} {M : Type u_4} (s : Finset ι) [CommMonoid M] (f : ι → M) :
∏ i : ↥s, f ↑i = ∏ i ∈ s, f i
source
theorem Finset.sum_coe_sort {ι : Type u_1} {M : Type u_4} (s : Finset ι) [AddCommMonoid M] (f : ι → M) :
∑ i : ↥s, f ↑i = ∑ i ∈ s, f i
source
theorem Finset.prod_finset_coe {ι : Type u_1} {M : Type u_4} [CommMonoid M] (f : ι → M) (s : Finset ι) :
∏ i : ↑↑s, f ↑i = ∏ i ∈ s, f i
source
theorem Finset.sum_finset_coe {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (f : ι → M) (s : Finset ι) :
∑ i : ↑↑s, f ↑i = ∑ i ∈ s, f i
source
theorem Finset.prod_subtype {ι : Type u_1} {M : Type u_4} [CommMonoid M] {p : ι → Prop} {F : Fintype (Subtype p)} (s : Finset ι) (h : ∀ (x : ι), x ∈ s ↔ p x) (f : ι → M) :
∏ a ∈ s, f a = ∏ a : Subtype p, f ↑a
source
theorem Finset.sum_subtype {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {p : ι → Prop} {F : Fintype (Subtype p)} (s : Finset ι) (h : ∀ (x : ι), x ∈ s ↔ p x) (f : ι → M) :
∑ a ∈ s, f a = ∑ a : Subtype p, f ↑a
source
theorem Finset.prod_set_coe {ι : Type u_1} {M : Type u_4} [CommMonoid M] {f : ι → M} (s : Set ι) [Fintype ↑s] :
∏ i : ↑s, f ↑i = ∏ i ∈ s.toFinset, f i
source
theorem Finset.sum_set_coe {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {f : ι → M} (s : Set ι) [Fintype ↑s] :
∑ i : ↑s, f ↑i = ∑ i ∈ s.toFinset, f i
source
theorem Finset.prod_congr_set {ι : Type u_1} {M : Type u_4} [CommMonoid M] [Fintype ι] (s : Set ι) [DecidablePred fun (x : ι) => x ∈ s] (f : ι → M) (g : ↑s → M) (w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩) (w' : ∀ x ∉ s, f x = 1) :
∏ i : ι, f i = ∏ i : ↑s, g i

The product of a function `g` defined only on a set `s` is equal to the product of a function `f` defined everywhere, as long as `f` and `g` agree on `s`, and `f = 1` off `s`.

source
theorem Finset.sum_congr_set {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Fintype ι] (s : Set ι) [DecidablePred fun (x : ι) => x ∈ s] (f : ι → M) (g : ↑s → M) (w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩) (w' : ∀ x ∉ s, f x = 0) :
∑ i : ι, f i = ∑ i : ↑s, g i

The sum of a function `g` defined only on a set `s` is equal to the sum of a function `f` defined everywhere, as long as `f` and `g` agree on `s`, and `f = 0` off `s`.

source
theorem Finset.prod_extend_by_one {ι : Type u_1} {M : Type u_4} [CommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι → M) :
(∏ i ∈ s, if i ∈ s then f i else 1) = ∏ i ∈ s, f i
source
theorem Finset.sum_extend_by_zero {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι → M) :
(∑ i ∈ s, if i ∈ s then f i else 0) = ∑ i ∈ s, f i
source
theorem Finset.prod_eq_prod_extend {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] (f : ↥s → M) :
∏ x : ↥s, f x = ∏ x ∈ s, Function.extend Subtype.val f 1 x
source
theorem Finset.sum_eq_sum_extend {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] (f : ↥s → M) :
∑ x : ↥s, f x = ∑ x ∈ s, Function.extend Subtype.val f 0 x
source
theorem Finset.prod_bij_ne_one {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (i : (a : ι) → a ∈ s → f a ≠ 1 → κ) (hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t) (i_inj : ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b) (h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)) :
∏ x ∈ s, f x = ∏ x ∈ t, g x
source
theorem Finset.sum_bij_ne_zero {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (i : (a : ι) → a ∈ s → f a ≠ 0 → κ) (hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 0), i a h₁ h₂ ∈ t) (i_inj : ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 0) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 0), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂) (i_surj : ∀ b ∈ t, g b ≠ 0 → ∃ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 0), i a h₁ h₂ = b) (h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 0), f a = g (i a h₁ h₂)) :
∑ x ∈ s, f x = ∑ x ∈ t, g x
source
theorem Finset.exists_ne_one_of_prod_ne_one {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : ι → M} (h : ∏ x ∈ s, f x ≠ 1) :
∃ a ∈ s, f a ≠ 1
source
theorem Finset.exists_ne_zero_of_sum_ne_zero {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (h : ∑ x ∈ s, f x ≠ 0) :
∃ a ∈ s, f a ≠ 0
source
theorem Finset.prod_range_succ_comm {M : Type u_4} [CommMonoid M] (f : ℕ → M) (n : ℕ) :
∏ x ∈ range (n + 1), f x = f n * ∏ x ∈ range n, f x
source
theorem Finset.sum_range_succ_comm {M : Type u_4} [AddCommMonoid M] (f : ℕ → M) (n : ℕ) :
∑ x ∈ range (n + 1), f x = f n + ∑ x ∈ range n, f x
source
theorem Finset.prod_range_succ {M : Type u_4} [CommMonoid M] (f : ℕ → M) (n : ℕ) :
∏ x ∈ range (n + 1), f x = (∏ x ∈ range n, f x) * f n
source
theorem Finset.sum_range_succ {M : Type u_4} [AddCommMonoid M] (f : ℕ → M) (n : ℕ) :
∑ x ∈ range (n + 1), f x = ∑ x ∈ range n, f x + f n
source
theorem Finset.prod_range_succ' {M : Type u_4} [CommMonoid M] (f : ℕ → M) (n : ℕ) :
∏ k ∈ range (n + 1), f k = (∏ k ∈ range n, f (k + 1)) * f 0
source
theorem Finset.sum_range_succ' {M : Type u_4} [AddCommMonoid M] (f : ℕ → M) (n : ℕ) :
∑ k ∈ range (n + 1), f k = ∑ k ∈ range n, f (k + 1) + f 0
source
theorem Finset.eventually_constant_prod {M : Type u_4} [CommMonoid M] {u : ℕ → M} {N : ℕ} (hu : ∀ n ≥ N, u n = 1) {n : ℕ} (hn : N ≤ n) :
∏ k ∈ range n, u k = ∏ k ∈ range N, u k
source
theorem Finset.eventually_constant_sum {M : Type u_4} [AddCommMonoid M] {u : ℕ → M} {N : ℕ} (hu : ∀ n ≥ N, u n = 0) {n : ℕ} (hn : N ≤ n) :
∑ k ∈ range n, u k = ∑ k ∈ range N, u k
source
theorem Finset.prod_range_add {M : Type u_4} [CommMonoid M] (f : ℕ → M) (n m : ℕ) :
∏ x ∈ range (n + m), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range m, f (n + x)
source
theorem Finset.sum_range_add {M : Type u_4} [AddCommMonoid M] (f : ℕ → M) (n m : ℕ) :
∑ x ∈ range (n + m), f x = ∑ x ∈ range n, f x + ∑ x ∈ range m, f (n + x)
source
theorem Finset.prod_range_one {M : Type u_4} [CommMonoid M] (f : ℕ → M) :
∏ k ∈ range 1, f k = f 0
source
theorem Finset.sum_range_one {M : Type u_4} [AddCommMonoid M] (f : ℕ → M) :
∑ k ∈ range 1, f k = f 0
source
theorem Finset.prod_list_map_count {ι : Type u_1} {M : Type u_4} [CommMonoid M] [DecidableEq ι] (l : List ι) (f : ι → M) :
(List.map f l).prod = ∏ m ∈ l.toFinset, f m ^ List.count m l
source
theorem Finset.sum_list_map_count {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] (l : List ι) (f : ι → M) :
(List.map f l).sum = ∑ m ∈ l.toFinset, List.count m l • f m
source
theorem Finset.prod_list_count {M : Type u_4} [CommMonoid M] [DecidableEq M] (s : List M) :
s.prod = ∏ m ∈ s.toFinset, m ^ List.count m s
source
theorem Finset.sum_list_count {M : Type u_4} [AddCommMonoid M] [DecidableEq M] (s : List M) :
s.sum = ∑ m ∈ s.toFinset, List.count m s • m
source
theorem Finset.prod_list_count_of_subset {M : Type u_4} [CommMonoid M] [DecidableEq M] (m : List M) (s : Finset M) (hs : m.toFinset ⊆ s) :
m.prod = ∏ i ∈ s, i ^ List.count i m
source
theorem Finset.sum_list_count_of_subset {M : Type u_4} [AddCommMonoid M] [DecidableEq M] (m : List M) (s : Finset M) (hs : m.toFinset ⊆ s) :
m.sum = ∑ i ∈ s, List.count i m • i
source
theorem Finset.prod_multiset_map_count {ι : Type u_1} [DecidableEq ι] (s : Multiset ι) {M : Type u_5} [CommMonoid M] (f : ι → M) :
(Multiset.map f s).prod = ∏ m ∈ s.toFinset, f m ^ Multiset.count m s
source
theorem Finset.sum_multiset_map_count {ι : Type u_1} [DecidableEq ι] (s : Multiset ι) {M : Type u_5} [AddCommMonoid M] (f : ι → M) :
(Multiset.map f s).sum = ∑ m ∈ s.toFinset, Multiset.count m s • f m
source
theorem Finset.prod_multiset_count {M : Type u_4} [CommMonoid M] [DecidableEq M] (s : Multiset M) :
s.prod = ∏ m ∈ s.toFinset, m ^ Multiset.count m s
source
theorem Finset.sum_multiset_count {M : Type u_4} [AddCommMonoid M] [DecidableEq M] (s : Multiset M) :
s.sum = ∑ m ∈ s.toFinset, Multiset.count m s • m
source
theorem Finset.prod_multiset_count_of_subset {M : Type u_4} [CommMonoid M] [DecidableEq M] (m : Multiset M) (s : Finset M) (hs : m.toFinset ⊆ s) :
m.prod = ∏ i ∈ s, i ^ Multiset.count i m
source
theorem Finset.sum_multiset_count_of_subset {M : Type u_4} [AddCommMonoid M] [DecidableEq M] (m : Multiset M) (s : Finset M) (hs : m.toFinset ⊆ s) :
m.sum = ∑ i ∈ s, Multiset.count i m • i
source
theorem Finset.prod_range_induction {M : Type u_4} [CommMonoid M] (f s : ℕ → M) (base : s 0 = 1) (n : ℕ) (step : ∀ k < n, s (k + 1) = s k * f k) :
∏ k ∈ 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 up to `n`.

This is a multiplicative discrete analogue of the fundamental theorem of calculus.

source
theorem Finset.sum_range_induction {M : Type u_4} [AddCommMonoid M] (f s : ℕ → M) (base : s 0 = 0) (n : ℕ) (step : ∀ k < n, s (k + 1) = s k + f k) :
∑ k ∈ 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 up to `n`.

This is a discrete analogue of the fundamental theorem of calculus.

source
@[simp]
theorem Finset.prod_const {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] (b : M) :
∏ _x ∈ s, b = b ^ s.card
source
@[simp]
theorem Finset.sum_const {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] (b : M) :
∑ _x ∈ s, b = s.card • b
source
theorem Finset.prod_eq_pow_card {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : ι → M} {b : M} (hf : ∀ a ∈ s, f a = b) :
∏ a ∈ s, f a = b ^ s.card
source
theorem Finset.sum_eq_card_nsmul {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} {b : M} (hf : ∀ a ∈ s, f a = b) :
∑ a ∈ s, f a = s.card • b
source
theorem Finset.pow_card_mul_prod {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : ι → M} {b : M} :
b ^ s.card * ∏ a ∈ s, f a = ∏ a ∈ s, b * f a
source
theorem Finset.card_nsmul_add_sum {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} {b : M} :
s.card • b + ∑ a ∈ s, f a = ∑ a ∈ s, (b + f a)
source
theorem Finset.prod_mul_pow_card {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : ι → M} {b : M} :
(∏ a ∈ s, f a) * b ^ s.card = ∏ a ∈ s, f a * b
source
theorem Finset.sum_add_card_nsmul {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} {b : M} :
∑ a ∈ s, f a + s.card • b = ∑ a ∈ s, (f a + b)
source
theorem Finset.pow_eq_prod_const {M : Type u_4} [CommMonoid M] (b : M) (n : ℕ) :
b ^ n = ∏ _k ∈ range n, b
source
theorem Finset.nsmul_eq_sum_const {M : Type u_4} [AddCommMonoid M] (b : M) (n : ℕ) :
n • b = ∑ _k ∈ range n, b
source
theorem Finset.prod_pow_eq_pow_sum {ι : Type u_1} {M : Type u_4} [CommMonoid M] (s : Finset ι) (f : ι → ℕ) (a : M) :
∏ i ∈ s, a ^ f i = a ^ ∑ i ∈ s, f i
source
theorem Finset.sum_nsmul_assoc {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] (s : Finset ι) (f : ι → ℕ) (a : M) :
∑ i ∈ s, f i • a = (∑ i ∈ s, f i) • a
source
theorem Finset.prod_flip {M : Type u_4} [CommMonoid M] {n : ℕ} (f : ℕ → M) :
∏ r ∈ range (n + 1), f (n - r) = ∏ k ∈ range (n + 1), f k
source
theorem Finset.sum_flip {M : Type u_4} [AddCommMonoid M] {n : ℕ} (f : ℕ → M) :
∑ r ∈ range (n + 1), f (n - r) = ∑ k ∈ range (n + 1), f k
source
theorem Finset.prod_involution {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : ι → M} (g : (a : ι) → a ∈ s → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1) (hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s) (hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a) :
∏ x ∈ s, f x = 1

The difference with `Finset.prod_ninvolution` is that the involution is allowed to use membership of the domain of the product, rather than being a non-dependent function.

source
theorem Finset.sum_involution {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (g : (a : ι) → a ∈ s → ι) (hg₁ : ∀ (a : ι) (ha : a ∈ s), f a + f (g a ha) = 0) (hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 0 → g a ha ≠ a) (g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s) (hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a) :
∑ x ∈ s, f x = 0

The difference with `Finset.sum_ninvolution` is that the involution is allowed to use membership of the domain of the sum, rather than being a non-dependent function.

source
theorem Finset.prod_ninvolution {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : ι → M} (g : ι → ι) (hg₁ : ∀ (a : ι), f a * f (g a) = 1) (hg₂ : ∀ (a : ι), f a ≠ 1 → g a ≠ a) (g_mem : ∀ (a : ι), g a ∈ s) (hg₃ : ∀ (a : ι), g (g a) = a) :
∏ x ∈ s, f x = 1

The difference with `Finset.prod_involution` is that the involution is a non-dependent function, rather than being allowed to use membership of the domain of the product.

source
theorem Finset.sum_ninvolution {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (g : ι → ι) (hg₁ : ∀ (a : ι), f a + f (g a) = 0) (hg₂ : ∀ (a : ι), f a ≠ 0 → g a ≠ a) (g_mem : ∀ (a : ι), g a ∈ s) (hg₃ : ∀ (a : ι), g (g a) = a) :
∑ x ∈ s, f x = 0

The difference with `Finset.sum_involution` is that the involution is a non-dependent function, rather than being allowed to use membership of the domain of the sum.

source
theorem Finset.prod_comp {ι : Type u_1} {κ : Type u_2} {M : Type u_4} {s : Finset ι} [CommMonoid M] [DecidableEq κ] (f : κ → M) (g : ι → κ) :
∏ a ∈ s, f (g a) = ∏ b ∈ image g s, f b ^ {a ∈ s | g a = b}.card

The product of the composition of functions `f` and `g`, is the product over `b ∈ s.image g` of `f b` to the power of the cardinality of the fibre of `b`. See also `Finset.prod_image`.

source
theorem Finset.sum_comp {ι : Type u_1} {κ : Type u_2} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] [DecidableEq κ] (f : κ → M) (g : ι → κ) :
∑ a ∈ s, f (g a) = ∑ b ∈ image g s, {a ∈ s | g a = b}.card • f b

The sum of the composition of functions `f` and `g`, is the sum over `b ∈ s.image g` of `f b` times of the cardinality of the fibre of `b`. See also `Finset.sum_image`.

source
theorem Finset.prod_partition {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : ι → M} (R : Setoid ι) [DecidableRel ⇑R] :
∏ x ∈ s, f x = ∏ xbar ∈ image (Quotient.mk R) s, ∏ y ∈ s with ⟦y⟧ = xbar, f y

A product can be partitioned into a product of products, each equivalent under a setoid.

source
theorem Finset.sum_partition {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (R : Setoid ι) [DecidableRel ⇑R] :
∑ x ∈ s, f x = ∑ xbar ∈ image (Quotient.mk R) s, ∑ y ∈ s with ⟦y⟧ = xbar, f y

A sum can be partitioned into a sum of sums, each equivalent under a setoid.

source
theorem Finset.prod_cancels_of_partition_cancels {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : ι → M} (R : Setoid ι) [DecidableRel ⇑R] (h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1) :
∏ x ∈ s, f x = 1

If we can partition a product into subsets that cancel out, then the whole product cancels.

source
theorem Finset.sum_cancels_of_partition_cancels {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (R : Setoid ι) [DecidableRel ⇑R] (h : ∀ x ∈ s, ∑ a ∈ s with R a x, f a = 0) :
∑ x ∈ s, f x = 0

If we can partition a sum into subsets that cancel out, then the whole sum cancels.

source
theorem Finset.eq_of_card_le_one_of_prod_eq {ι : Type u_1} {M : Type u_4} [CommMonoid M] {s : Finset ι} (hc : s.card ≤ 1) {f : ι → M} {b : M} (h : ∏ x ∈ s, f x = b) (x : ι) :
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.

source
theorem Finset.eq_of_card_le_one_of_sum_eq {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} (hc : s.card ≤ 1) {f : ι → M} {b : M} (h : ∑ x ∈ s, f x = b) (x : ι) :
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.

source
theorem Finset.mul_prod_erase {ι : Type u_1} {M : Type u_4} [CommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι} (h : a ∈ s) :
f a * ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x

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

See `Multiset.prod_map_erase` for the `Multiset` version.

source
theorem Finset.add_sum_erase {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι} (h : a ∈ s) :
f a + ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x

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

See `Multiset.sum_map_erase` for the `Multiset` version.

source
theorem Finset.prod_erase_mul {ι : Type u_1} {M : Type u_4} [CommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι} (h : a ∈ s) :
(∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x

A variant of `Finset.mul_prod_erase` with the multiplication swapped.

source
theorem Finset.sum_erase_add {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι} (h : a ∈ s) :
∑ x ∈ s.erase a, f x + f a = ∑ x ∈ s, f x

A variant of `Finset.add_sum_erase` with the addition swapped.

source
theorem Finset.prod_erase {ι : Type u_1} {M : Type u_4} [CommMonoid M] [DecidableEq ι] (s : Finset ι) {f : ι → M} {a : ι} (h : f a = 1) :
∏ x ∈ s.erase a, f x = ∏ x ∈ 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`.

source
theorem Finset.sum_erase {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] (s : Finset ι) {f : ι → M} {a : ι} (h : f a = 0) :
∑ x ∈ s.erase a, f x = ∑ x ∈ 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`.

source
theorem Finset.prod_erase_lt_of_one_lt {ι : Type u_1} {κ : Type u_5} [DecidableEq ι] [CommMonoid κ] [LT κ] [MulLeftStrictMono κ] {s : Finset ι} {d : ι} (hd : d ∈ s) {f : ι → κ} (hdf : 1 < f d) :
∏ m ∈ s.erase d, f m < ∏ m ∈ s, f m
source
theorem Finset.sum_erase_lt_of_pos {ι : Type u_1} {κ : Type u_5} [DecidableEq ι] [AddCommMonoid κ] [LT κ] [AddLeftStrictMono κ] {s : Finset ι} {d : ι} (hd : d ∈ s) {f : ι → κ} (hdf : 0 < f d) :
∑ m ∈ s.erase d, f m < ∑ m ∈ s, f m
source
theorem Finset.eq_one_of_prod_eq_one {ι : Type u_1} {M : Type u_4} [CommMonoid M] {s : Finset ι} {f : ι → M} {a : ι} (hp : ∏ x ∈ s, f x = 1) (h1 : ∀ x ∈ s, x ≠ a → f x = 1) (x : ι) :
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`.

source
theorem Finset.eq_zero_of_sum_eq_zero {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {f : ι → M} {a : ι} (hp : ∑ x ∈ s, f x = 0) (h1 : ∀ x ∈ s, x ≠ a → f x = 0) (x : ι) :
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`.

source
theorem Finset.prod_mul_eq_prod_mul_of_exists {ι : Type u_1} {M : Type u_4} [CommMonoid M] {s : Finset ι} {f : ι → M} {b₁ b₂ : M} (a : ι) (ha : a ∈ s) (h : f a * b₁ = f a * b₂) :
(∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂
source
theorem Finset.sum_add_eq_sum_add_of_exists {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] {s : Finset ι} {f : ι → M} {b₁ b₂ : M} (a : ι) (ha : a ∈ s) (h : f a + b₁ = f a + b₂) :
∑ a ∈ s, f a + b₁ = ∑ a ∈ s, f a + b₂
source
theorem Finset.prod_filter_of_pairwise_eq_one {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] [DecidableEq ι] {f : κ → ι} {g : ι → M} {n : κ} {I : Finset κ} (hn : n ∈ I) (hf : (↑I).Pairwise fun (i j : κ) => f i = f j → g (f i) = 1) :
∏ j ∈ I with f j = f n, g (f j) = g (f n)
source
theorem Finset.sum_filter_of_pairwise_eq_zero {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] {f : κ → ι} {g : ι → M} {n : κ} {I : Finset κ} (hn : n ∈ I) (hf : (↑I).Pairwise fun (i j : κ) => f i = f j → g (f i) = 0) :
∑ j ∈ I with f j = f n, g (f j) = g (f n)
source
@[simp]
theorem Finset.prod_image_of_pairwise_eq_one {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] [DecidableEq ι] {f : κ → ι} {g : ι → M} {I : Finset κ} (hf : (↑I).Pairwise fun (i j : κ) => f i = f j → g (f i) = 1) :
∏ s ∈ image f I, g s = ∏ i ∈ I, g (f i)

A version of `Finset.prod_map` and `Finset.prod_image`, but we do not assume that `f` is injective. Rather, we assume that the image of `f` on `I` only overlaps where `g (f i) = 1`. The conclusion is the same as in `prod_image`.

source
@[simp]
theorem Finset.sum_image_of_pairwise_eq_zero {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] {f : κ → ι} {g : ι → M} {I : Finset κ} (hf : (↑I).Pairwise fun (i j : κ) => f i = f j → g (f i) = 0) :
∑ s ∈ image f I, g s = ∑ i ∈ I, g (f i)

A version of `Finset.sum_map` and `Finset.sum_image`, but we do not assume that `f` is injective. Rather, we assume that the image of `f` on `I` only overlaps where `g (f i) = 0`. The conclusion is the same as in `sum_image`.

source
@[simp]
theorem Finset.prod_image_of_disjoint {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [CommMonoid M] [DecidableEq ι] [PartialOrder ι] [OrderBot ι] {f : κ → ι} {g : ι → M} (hg_bot : g ⊥ = 1) {I : Finset κ} (hf_disj : (↑I).PairwiseDisjoint f) :
∏ s ∈ image f I, g s = ∏ i ∈ I, g (f i)

A version of `Finset.prod_map` and `Finset.prod_image`, but we do not assume that `f` is injective. Rather, we assume that the images of `f` are disjoint on `I`, and `g ⊥ = 1`. The conclusion is the same as in `prod_image`.

source
@[simp]
theorem Finset.sum_image_of_disjoint {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [AddCommMonoid M] [DecidableEq ι] [PartialOrder ι] [OrderBot ι] {f : κ → ι} {g : ι → M} (hg_bot : g ⊥ = 0) {I : Finset κ} (hf_disj : (↑I).PairwiseDisjoint f) :
∑ s ∈ image f I, g s = ∑ i ∈ I, g (f i)

A version of `Finset.sum_map` and `Finset.sum_image`, but we do not assume that `f` is injective. Rather, we assume that the images of `f` are disjoint on `I`, and `g ⊥ = 0`. The conclusion is the same as in `sum_image`.

source
theorem Finset.prod_unique_nonempty {ι : Type u_1} {M : Type u_4} [CommMonoid M] [Unique ι] (s : Finset ι) (f : ι → M) (h : s.Nonempty) :
∏ x ∈ s, f x = f default
source
theorem Finset.sum_unique_nonempty {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [Unique ι] (s : Finset ι) (f : ι → M) (h : s.Nonempty) :
∑ x ∈ s, f x = f default
source
theorem Finset.prod_dvd_prod_of_dvd {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] (f g : ι → M) (h : ∀ i ∈ s, f i ∣ g i) :
∏ i ∈ s, f i ∣ ∏ i ∈ s, g i
source
theorem Finset.prod_map_equiv {ι : Type u_1} {κ : Type u_2} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : ι → M} (e : ι ≃ κ) :
(map e.toEmbedding s).prod (f ∘ ⇑e.symm) = s.prod f
source
theorem Finset.sum_map_equiv {ι : Type u_1} {κ : Type u_2} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} (e : ι ≃ κ) :
(map e.toEmbedding s).sum (f ∘ ⇑e.symm) = s.sum f
source
theorem Finset.prod_comp_equiv {ι : Type u_1} {κ : Type u_2} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : κ → M} (e : ι ≃ κ) :
s.prod (f ∘ ⇑e) = (map e.toEmbedding s).prod f
source
theorem Finset.sum_comp_equiv {ι : Type u_1} {κ : Type u_2} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : κ → M} (e : ι ≃ κ) :
s.sum (f ∘ ⇑e) = (map e.toEmbedding s).sum f
source
theorem Finset.prod_sdiff_eq_prod_sdiff_iff {ι : Type u_1} {M : Type u_4} [DecidableEq ι] [CancelCommMonoid M] {s t : Finset ι} {f : ι → M} :
∏ i ∈ s \ t, f i = ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i = ∏ i ∈ t, f i
source
theorem Finset.sum_sdiff_eq_sum_sdiff_iff {ι : Type u_1} {M : Type u_4} [DecidableEq ι] [AddCancelCommMonoid M] {s t : Finset ι} {f : ι → M} :
∑ i ∈ s \ t, f i = ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i = ∑ i ∈ t, f i
source
theorem Finset.prod_sdiff_ne_prod_sdiff_iff {ι : Type u_1} {M : Type u_4} [DecidableEq ι] [CancelCommMonoid M] {s t : Finset ι} {f : ι → M} :
∏ i ∈ s \ t, f i ≠ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≠ ∏ i ∈ t, f i
source
theorem Finset.sum_sdiff_ne_sum_sdiff_iff {ι : Type u_1} {M : Type u_4} [DecidableEq ι] [AddCancelCommMonoid M] {s t : Finset ι} {f : ι → M} :
∑ i ∈ s \ t, f i ≠ ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i ≠ ∑ i ∈ t, f i
source
theorem Finset.prod_insert_div {ι : Type u_1} {G : Type u_3} {s : Finset ι} {a : ι} [CommGroup G] [DecidableEq ι] (ha : a ∉ s) (f : ι → G) :
(∏ x ∈ insert a s, f x) / f a = ∏ x ∈ s, f x
source
theorem Finset.sum_insert_sub {ι : Type u_1} {G : Type u_3} {s : Finset ι} {a : ι} [AddCommGroup G] [DecidableEq ι] (ha : a ∉ s) (f : ι → G) :
∑ x ∈ insert a s, f x - f a = ∑ x ∈ s, f x
source
@[simp]
theorem Finset.prod_erase_eq_div {ι : Type u_1} {G : Type u_3} {s : Finset ι} [CommGroup G] [DecidableEq ι] {f : ι → G} {a : ι} (h : a ∈ s) :
∏ x ∈ s.erase a, f x = (∏ x ∈ s, f x) / f a
source
@[simp]
theorem Finset.sum_erase_eq_sub {ι : Type u_1} {G : Type u_3} {s : Finset ι} [AddCommGroup G] [DecidableEq ι] {f : ι → G} {a : ι} (h : a ∈ s) :
∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x - f a
source
theorem Finset.prod_range_div {G : Type u_3} [CommGroup G] (f : ℕ → G) (n : ℕ) :
∏ i ∈ 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.

source
theorem Finset.sum_range_sub {G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n : ℕ) :
∑ i ∈ range n, (f (i + 1) - f i) = f n - f 0

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

source
theorem Finset.prod_range_div' {G : Type u_3} [CommGroup G] (f : ℕ → G) (n : ℕ) :
∏ i ∈ range n, f i / f (i + 1) = f 0 / f n
source
theorem Finset.sum_range_sub' {G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n : ℕ) :
∑ i ∈ range n, (f i - f (i + 1)) = f 0 - f n
source
theorem Finset.eq_prod_range_div {G : Type u_3} [CommGroup G] (f : ℕ → G) (n : ℕ) :
f n = f 0 * ∏ i ∈ range n, f (i + 1) / f i
source
theorem Finset.eq_sum_range_sub {G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n : ℕ) :
f n = f 0 + ∑ i ∈ range n, (f (i + 1) - f i)
source
theorem Finset.eq_prod_range_div' {G : Type u_3} [CommGroup G] (f : ℕ → G) (n : ℕ) :
f n = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1)
source
theorem Finset.eq_sum_range_sub' {G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n : ℕ) :
f n = ∑ i ∈ range (n + 1), if i = 0 then f 0 else f i - f (i - 1)
source
theorem Finset.prod_range_add_div_prod_range {G : Type u_3} [CommGroup G] (f : ℕ → G) (n m : ℕ) :
(∏ k ∈ range (n + m), f k) / ∏ k ∈ range n, f k = ∏ k ∈ range m, f (n + k)
source
theorem Finset.sum_range_add_sub_sum_range {G : Type u_3} [AddCommGroup G] (f : ℕ → G) (n m : ℕ) :
∑ k ∈ range (n + m), f k - ∑ k ∈ range n, f k = ∑ k ∈ range m, f (n + k)
source
@[simp]
theorem Finset.prod_sdiff_eq_div {ι : Type u_1} {G : Type u_3} {s₁ s₂ : Finset ι} [CommGroup G] [DecidableEq ι] {f : ι → G} (h : s₁ ⊆ s₂) :
∏ x ∈ s₂ \ s₁, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x
source
@[simp]
theorem Finset.sum_sdiff_eq_sub {ι : Type u_1} {G : Type u_3} {s₁ s₂ : Finset ι} [AddCommGroup G] [DecidableEq ι] {f : ι → G} (h : s₁ ⊆ s₂) :
∑ x ∈ s₂ \ s₁, f x = ∑ x ∈ s₂, f x - ∑ x ∈ s₁, f x
source
theorem Finset.prod_sdiff_div_prod_sdiff {ι : Type u_1} {G : Type u_3} {s₁ s₂ : Finset ι} [CommGroup G] [DecidableEq ι] {f : ι → G} :
(∏ x ∈ s₂ \ s₁, f x) / ∏ x ∈ s₁ \ s₂, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x
source
theorem Finset.sum_sdiff_sub_sum_sdiff {ι : Type u_1} {G : Type u_3} {s₁ s₂ : Finset ι} [AddCommGroup G] [DecidableEq ι] {f : ι → G} :
∑ x ∈ s₂ \ s₁, f x - ∑ x ∈ s₁ \ s₂, f x = ∑ x ∈ s₂, f x - ∑ x ∈ s₁, f x
source
theorem Finset.sum_range_tsub {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [Sub M] [OrderedSub M] [AddLeftMono M] [AddLeftReflectLE M] [ExistsAddOfLE M] {f : ℕ → M} (h : Monotone f) (n : ℕ) :
∑ i ∈ 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.

source
theorem Finset.sum_tsub_distrib {ι : Type u_1} {M : Type u_4} [AddCommMonoid M] [PartialOrder M] [Sub M] [OrderedSub M] [AddLeftMono M] [AddLeftReflectLE M] [ExistsAddOfLE M] (s : Finset ι) {f g : ι → M} (hfg : ∀ x ∈ s, g x ≤ f x) :
∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x - ∑ x ∈ s, g x
source
theorem Finset.card_eq_sum_ones {ι : Type u_1} (s : Finset ι) :
s.card = ∑ x ∈ s, 1
source
theorem Finset.sum_const_nat {ι : Type u_1} {s : Finset ι} {m : ℕ} {f : ι → ℕ} (h₁ : ∀ x ∈ s, f x = m) :
∑ x ∈ s, f x = s.card * m
source
theorem Finset.sum_card_fiberwise_eq_card_filter {ι : Type u_1} {κ : Type u_5} [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) :
∑ j ∈ t, {i ∈ s | g i = j}.card = {i ∈ s | g i ∈ t}.card
source
@[simp]
theorem Finset.card_disjiUnion {ι : Type u_1} {M : Type u_4} (s : Finset ι) (t : ι → Finset M) (h : (↑s).PairwiseDisjoint t) :
(s.disjiUnion t h).card = ∑ a ∈ s, (t a).card
source
theorem Finset.card_biUnion {ι : Type u_1} {M : Type u_4} {s : Finset ι} [DecidableEq M] {t : ι → Finset M} (h : (↑s).PairwiseDisjoint t) :
(s.biUnion t).card = ∑ u ∈ s, (t u).card
source
theorem Finset.card_biUnion_le {ι : Type u_1} {M : Type u_4} [DecidableEq M] {s : Finset ι} {t : ι → Finset M} :
(s.biUnion t).card ≤ ∑ a ∈ s, (t a).card
source
theorem Finset.card_eq_sum_card_fiberwise {ι : Type u_1} {M : Type u_4} [DecidableEq M] {f : ι → M} {s : Finset ι} {t : Finset M} (H : Set.MapsTo f ↑s ↑t) :
s.card = ∑ b ∈ t, {a ∈ s | f a = b}.card
source
theorem Finset.card_eq_sum_card_image {ι : Type u_1} {M : Type u_4} [DecidableEq M] (f : ι → M) (s : Finset ι) :
s.card = ∑ b ∈ image f s, {a ∈ s | f a = b}.card
source
theorem Fintype.prod_of_injective {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [Fintype ι] [Fintype κ] [CommMonoid M] (e : ι → κ) (he : Function.Injective e) (f : ι → M) (g : κ → M) (h' : ∀ i ∉ Set.range e, g i = 1) (h : ∀ (i : ι), f i = g (e i)) :
∏ i : ι, f i = ∏ j : κ, g j
source
theorem Fintype.sum_of_injective {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [Fintype ι] [Fintype κ] [AddCommMonoid M] (e : ι → κ) (he : Function.Injective e) (f : ι → M) (g : κ → M) (h' : ∀ i ∉ Set.range e, g i = 0) (h : ∀ (i : ι), f i = g (e i)) :
∑ i : ι, f i = ∑ j : κ, g j
source
theorem Fintype.prod_fiberwise {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [Fintype ι] [Fintype κ] [CommMonoid M] [DecidableEq κ] (g : ι → κ) (f : ι → M) :
∏ j : κ, ∏ i : { i : ι // g i = j }, f ↑i = ∏ i : ι, f i
source
theorem Fintype.sum_fiberwise {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [Fintype ι] [Fintype κ] [AddCommMonoid M] [DecidableEq κ] (g : ι → κ) (f : ι → M) :
∑ j : κ, ∑ i : { i : ι // g i = j }, f ↑i = ∑ i : ι, f i
source
theorem Fintype.prod_fiberwise' {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [Fintype ι] [Fintype κ] [CommMonoid M] [DecidableEq κ] (g : ι → κ) (f : κ → M) :
∏ j : κ, ∏ _i : { i : ι // g i = j }, f j = ∏ i : ι, f (g i)
source
theorem Fintype.sum_fiberwise' {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [Fintype ι] [Fintype κ] [AddCommMonoid M] [DecidableEq κ] (g : ι → κ) (f : κ → M) :
∑ j : κ, ∑ _i : { i : ι // g i = j }, f j = ∑ i : ι, f (g i)
source
theorem Fintype.prod_unique {M : Type u_4} {ι : Type u_7} [Fintype ι] [CommMonoid M] [Unique ι] (f : ι → M) :
∏ x : ι, f x = f default
source
theorem Fintype.sum_unique {M : Type u_4} {ι : Type u_7} [Fintype ι] [AddCommMonoid M] [Unique ι] (f : ι → M) :
∑ x : ι, f x = f default
source
theorem Fintype.prod_subsingleton {M : Type u_4} {ι : Type u_7} [Fintype ι] [CommMonoid M] [Subsingleton ι] (f : ι → M) (a : ι) :
∏ x : ι, f x = f a
source
theorem Fintype.sum_subsingleton {M : Type u_4} {ι : Type u_7} [Fintype ι] [AddCommMonoid M] [Subsingleton ι] (f : ι → M) (a : ι) :
∑ x : ι, f x = f a
source
theorem Fintype.prod_Prop {M : Type u_4} [CommMonoid M] (f : Prop → M) :
∏ p : Prop, f p = f True * f False
source
theorem Fintype.sum_Prop {M : Type u_4} [AddCommMonoid M] (f : Prop → M) :
∑ p : Prop, f p = f True + f False
source
theorem Fintype.prod_subtype_mul_prod_subtype {M : Type u_4} {ι : Type u_7} [Fintype ι] [CommMonoid M] (p : ι → Prop) (f : ι → M) [DecidablePred p] :
(∏ i : { x : ι // p x }, f ↑i) * ∏ i : { x : ι // ¬p x }, f ↑i = ∏ i : ι, f i
source
theorem Fintype.sum_subtype_add_sum_subtype {M : Type u_4} {ι : Type u_7} [Fintype ι] [AddCommMonoid M] (p : ι → Prop) (f : ι → M) [DecidablePred p] :
∑ i : { x : ι // p x }, f ↑i + ∑ i : { x : ι // ¬p x }, f ↑i = ∑ i : ι, f i
source
theorem Fintype.prod_subset {M : Type u_4} {ι : Type u_7} [Fintype ι] [CommMonoid M] {s : Finset ι} {f : ι → M} (h : ∀ (i : ι), f i ≠ 1 → i ∈ s) :
∏ i ∈ s, f i = ∏ i : ι, f i
source
theorem Fintype.sum_subset {M : Type u_4} {ι : Type u_7} [Fintype ι] [AddCommMonoid M] {s : Finset ι} {f : ι → M} (h : ∀ (i : ι), f i ≠ 0 → i ∈ s) :
∑ i ∈ s, f i = ∑ i : ι, f i
source
theorem List.prod_toFinset {ι : Type u_1} {M : Type u_5} [DecidableEq ι] [CommMonoid M] (f : ι → M) {l : List ι} (_hl : l.Nodup) :
l.toFinset.prod f = (map f l).prod
source
theorem List.sum_toFinset {ι : Type u_1} {M : Type u_5} [DecidableEq ι] [AddCommMonoid M] (f : ι → M) {l : List ι} (_hl : l.Nodup) :
l.toFinset.sum f = (map f l).sum
source
@[simp]
theorem List.sum_toFinset_count_eq_length {ι : Type u_1} [DecidableEq ι] (l : List ι) :
∑ a ∈ l.toFinset, count a l = l.length
source
@[simp]
theorem Multiset.mem_sum {ι : Type u_1} {M : Type u_4} {a : M} {s : Finset ι} {m : ι → Multiset M} :
a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i
source
@[deprecated Multiset.mem_sum (since := "2025-08-24")]
theorem Finset.mem_sum {ι : Type u_1} {M : Type u_4} {f : ι → Multiset M} (s : Finset ι) (b : M) :
b ∈ ∑ x ∈ s, f x ↔ ∃ a ∈ s, b ∈ f a
source
theorem Multiset.toFinset_sum_count_eq {ι : Type u_1} [DecidableEq ι] (s : Multiset ι) :
∑ a ∈ s.toFinset, count a s = s.card
source
@[simp]
theorem Multiset.sum_count_eq_card {ι : Type u_1} [DecidableEq ι] {s : Finset ι} {m : Multiset ι} (hms : ∀ a ∈ m, a ∈ s) :
∑ a ∈ s, count a m = m.card
source
@[simp]
theorem Multiset.toFinset_sum_count_nsmul_eq {ι : Type u_1} [DecidableEq ι] (s : Multiset ι) :
∑ a ∈ s.toFinset, count a s • {a} = s
source
theorem Multiset.exists_smul_of_dvd_count {ι : Type u_1} [DecidableEq ι] (s : Multiset ι) {k : ℕ} (h : ∀ a ∈ s, k ∣ count a s) :
∃ (u : Multiset ι), s = k • u
source
theorem Multiset.prod_sum {M : Type u_4} {ι : Type u_5} [CommMonoid M] (f : ι → Multiset M) (s : Finset ι) :
(∑ x ∈ s, f x).prod = ∏ x ∈ s, (f x).prod
source
theorem Multiset.sum_sum {M : Type u_4} {ι : Type u_5} [AddCommMonoid M] (f : ι → Multiset M) (s : Finset ι) :
(∑ x ∈ s, f x).sum = ∑ x ∈ s, (f x).sum
source
@[simp]
theorem IsUnit.prod_iff {ι : Type u_1} {M : Type u_4} {s : Finset ι} [CommMonoid M] {f : ι → M} :
IsUnit (∏ a ∈ s, f a) ↔ ∀ a ∈ s, IsUnit (f a)
source
@[simp]
theorem IsAddUnit.sum_iff {ι : Type u_1} {M : Type u_4} {s : Finset ι} [AddCommMonoid M] {f : ι → M} :
IsAddUnit (∑ a ∈ s, f a) ↔ ∀ a ∈ s, IsAddUnit (f a)
source
theorem IsUnit.prod_univ_iff {ι : Type u_1} {M : Type u_4} [Fintype ι] [CommMonoid M] {f : ι → M} :
IsUnit (∏ a : ι, f a) ↔ ∀ (a : ι), IsUnit (f a)
source
theorem IsAddUnit.sum_univ_iff {ι : Type u_1} {M : Type u_4} [Fintype ι] [AddCommMonoid M] {f : ι → M} :
IsAddUnit (∑ a : ι, f a) ↔ ∀ (a : ι), IsAddUnit (f a)
source
theorem nat_abs_sum_le {ι : Type u_1} (s : Finset ι) (f : ι → ℤ) :
(∑ i ∈ s, f i).natAbs ≤ ∑ i ∈ s, (f i).natAbs