Big operators

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

theorem Finset.prod_eq_fold {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : α → β) : ∏ x ∈ s, f x = fold (fun (x1 x2 : β) => x1 * x2) 1 f s

theorem Finset.sum_eq_fold {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : ∑ x ∈ s, f x = fold (fun (x1 x2 : β) => x1 + x2) 0 f s

@[simp]

theorem Finset.prod_cons {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [CommMonoid β] (h : a ∉ s) : ∏ x ∈ cons a s h, f x = f a * ∏ x ∈ s, f x

@[simp]

theorem Finset.sum_cons {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [AddCommMonoid β] (h : a ∉ s) : ∑ x ∈ cons a s h, f x = f a + ∑ x ∈ s, f x

@[simp]

theorem Finset.prod_insert {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [CommMonoid β] [DecidableEq α] : a ∉ s → ∏ x ∈ insert a s, f x = f a * ∏ x ∈ s, f x

@[simp]

theorem Finset.sum_insert {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [AddCommMonoid β] [DecidableEq α] : a ∉ s → ∑ x ∈ insert a s, f x = f a + ∑ x ∈ s, f x

@[simp]

theorem Finset.prod_insert_of_eq_one_if_not_mem {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [CommMonoid β] [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.

@[simp]

theorem Finset.sum_insert_of_eq_zero_if_not_mem {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [AddCommMonoid β] [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.

@[simp]

theorem Finset.prod_insert_one {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [CommMonoid β] [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.

@[simp]

theorem Finset.sum_insert_zero {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [AddCommMonoid β] [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.

theorem Finset.prod_insert_div {α : Type u_3} {s : Finset α} {a : α} {M : Type u_6} [CommGroup M] [DecidableEq α] (ha : a ∉ s) {f : α → M} : (∏ x ∈ insert a s, f x) / f a = ∏ x ∈ s, f x

theorem Finset.sum_insert_sub {α : Type u_3} {s : Finset α} {a : α} {M : Type u_6} [AddCommGroup M] [DecidableEq α] (ha : a ∉ s) {f : α → M} : ∑ x ∈ insert a s, f x - f a = ∑ x ∈ s, f x

@[simp]

theorem Finset.prod_singleton {α : Type u_3} {β : Type u_4} [CommMonoid β] (f : α → β) (a : α) : ∏ x ∈ {a}, f x = f a

@[simp]

theorem Finset.sum_singleton {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (f : α → β) (a : α) : ∑ x ∈ {a}, f x = f a

theorem Finset.prod_pair {α : Type u_3} {β : Type u_4} {f : α → β} [CommMonoid β] [DecidableEq α] {a b : α} (h : a ≠ b) : ∏ x ∈ {a, b}, f x = f a * f b

theorem Finset.sum_pair {α : Type u_3} {β : Type u_4} {f : α → β} [AddCommMonoid β] [DecidableEq α] {a b : α} (h : a ≠ b) : ∑ x ∈ {a, b}, f x = f a + f b

@[simp]

theorem Finset.prod_image {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β} [CommMonoid β] [DecidableEq α] {s : Finset γ} {g : γ → α} : (∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) → ∏ x ∈ image g s, f x = ∏ x ∈ s, f (g x)

@[simp]

theorem Finset.sum_image {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β} [AddCommMonoid β] [DecidableEq α] {s : Finset γ} {g : γ → α} : (∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) → ∑ x ∈ image g s, f x = ∑ x ∈ s, f (g x)

theorem Finset.prod_attach {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : α → β) : ∏ x ∈ s.attach, f ↑x = ∏ x ∈ s, f x

theorem Finset.sum_attach {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : ∑ x ∈ s.attach, f ↑x = ∑ x ∈ s, f x

theorem Finset.prod_congr {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f g : α → β} [CommMonoid β] (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g

theorem Finset.sum_congr {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f g : α → β} [AddCommMonoid β] (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.sum f = s₂.sum g

theorem Finset.prod_eq_one {α : Type u_3} {β : Type u_4} [CommMonoid β] {f : α → β} {s : Finset α} (h : ∀ x ∈ s, f x = 1) : ∏ x ∈ s, f x = 1

theorem Finset.sum_eq_zero {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {f : α → β} {s : Finset α} (h : ∀ x ∈ s, f x = 0) : ∑ x ∈ s, f x = 0

theorem Finset.prod_disjUnion {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [CommMonoid β] (h : Disjoint s₁ s₂) : ∏ x ∈ s₁.disjUnion s₂ h, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x

theorem Finset.sum_disjUnion {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [AddCommMonoid β] (h : Disjoint s₁ s₂) : ∑ x ∈ s₁.disjUnion s₂ h, f x = ∑ x ∈ s₁, f x + ∑ x ∈ s₂, f x

theorem Finset.prod_disjiUnion {ι : Type u_1} {α : Type u_3} {β : Type u_4} {f : α → β} [CommMonoid β] (s : Finset ι) (t : ι → Finset α) (h : (↑s).PairwiseDisjoint t) : ∏ x ∈ s.disjiUnion t h, f x = ∏ i ∈ s, ∏ x ∈ t i, f x

theorem Finset.sum_disjiUnion {ι : Type u_1} {α : Type u_3} {β : Type u_4} {f : α → β} [AddCommMonoid β] (s : Finset ι) (t : ι → Finset α) (h : (↑s).PairwiseDisjoint t) : ∑ x ∈ s.disjiUnion t h, f x = ∑ i ∈ s, ∑ x ∈ t i, f x

theorem Finset.prod_union_inter {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [CommMonoid β] [DecidableEq α] : (∏ x ∈ s₁ ∪ s₂, f x) * ∏ x ∈ s₁ ∩ s₂, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x

theorem Finset.sum_union_inter {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [AddCommMonoid β] [DecidableEq α] : ∑ x ∈ s₁ ∪ s₂, f x + ∑ x ∈ s₁ ∩ s₂, f x = ∑ x ∈ s₁, f x + ∑ x ∈ s₂, f x

theorem Finset.prod_union {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [CommMonoid β] [DecidableEq α] (h : Disjoint s₁ s₂) : ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x

theorem Finset.sum_union {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [AddCommMonoid β] [DecidableEq α] (h : Disjoint s₁ s₂) : ∑ x ∈ s₁ ∪ s₂, f x = ∑ x ∈ s₁, f x + ∑ x ∈ s₂, f x

theorem Finset.prod_filter_mul_prod_filter_not {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] (f : α → β) : (∏ x ∈ {x ∈ s | p x}, f x) * ∏ x ∈ {x ∈ s | ¬p x}, f x = ∏ x ∈ s, f x

theorem Finset.sum_filter_add_sum_filter_not {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] (f : α → β) : ∑ x ∈ {x ∈ s | p x}, f x + ∑ x ∈ {x ∈ s | ¬p x}, f x = ∑ x ∈ s, f x

theorem Finset.prod_filter_not_mul_prod_filter {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] (f : α → β) : (∏ x ∈ {x ∈ s | ¬p x}, f x) * ∏ x ∈ {x ∈ s | p x}, f x = ∏ x ∈ s, f x

theorem Finset.sum_filter_not_add_sum_filter {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (p : α → Prop) [DecidablePred p] [(x : α) → Decidable ¬p x] (f : α → β) : ∑ x ∈ {x ∈ s | ¬p x}, f x + ∑ x ∈ {x ∈ s | p x}, f x = ∑ x ∈ s, f x

theorem Finset.prod_filter_xor {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] (p q : α → Prop) [DecidablePred p] [DecidablePred q] : ∏ x ∈ {x ∈ s | Xor' (p x) (q x)}, f x = (∏ x ∈ {x ∈ s | p x ∧ ¬q x}, f x) * ∏ x ∈ {x ∈ s | q x ∧ ¬p x}, f x

theorem Finset.sum_filter_xor {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] (p q : α → Prop) [DecidablePred p] [DecidablePred q] : ∑ x ∈ {x ∈ s | Xor' (p x) (q x)}, f x = ∑ x ∈ {x ∈ s | p x ∧ ¬q x}, f x + ∑ x ∈ {x ∈ s | q x ∧ ¬p x}, f x

@[simp]

theorem Finset.prod_eq_one_iff {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] [Subsingleton βˣ] : ∏ 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.

@[simp]

theorem Finset.sum_eq_zero_iff {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] [Subsingleton (AddUnits β)] : ∑ i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0

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

@[deprecated Finset.prod_eq_one_iff (since := "2025-03-31")]

theorem Finset.prod_eq_one_iff' {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] [Subsingleton βˣ] : ∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1

Alias of Finset.prod_eq_one_iff.

---

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

theorem IsCompl.prod_mul_prod {α : Type u_3} {β : Type u_4} [CommMonoid β] [Fintype α] {s t : Finset α} (h : IsCompl s t) (f : α → β) : (∏ i ∈ s, f i) * ∏ i ∈ t, f i = ∏ i : α, f i

theorem IsCompl.sum_add_sum {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [Fintype α] {s t : Finset α} (h : IsCompl s t) (f : α → β) : ∑ i ∈ s, f i + ∑ i ∈ t, f i = ∑ i : α, f i

theorem Finset.prod_mul_prod_compl {α : Type u_3} {β : Type u_4} [CommMonoid β] [Fintype α] [DecidableEq α] (s : Finset α) (f : α → β) : (∏ 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.

theorem Finset.sum_add_sum_compl {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [Fintype α] [DecidableEq α] (s : Finset α) (f : α → β) : ∑ 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.

theorem Finset.prod_compl_mul_prod {α : Type u_3} {β : Type u_4} [CommMonoid β] [Fintype α] [DecidableEq α] (s : Finset α) (f : α → β) : (∏ i ∈ sᶜ, f i) * ∏ i ∈ s, f i = ∏ i : α, f i

theorem Finset.sum_compl_add_sum {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [Fintype α] [DecidableEq α] (s : Finset α) (f : α → β) : ∑ i ∈ sᶜ, f i + ∑ i ∈ s, f i = ∑ i : α, f i

theorem Finset.prod_sdiff {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [CommMonoid β] [DecidableEq α] (h : s₁ ⊆ s₂) : (∏ x ∈ s₂ \ s₁, f x) * ∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x

theorem Finset.sum_sdiff {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [AddCommMonoid β] [DecidableEq α] (h : s₁ ⊆ s₂) : ∑ x ∈ s₂ \ s₁, f x + ∑ x ∈ s₁, f x = ∑ x ∈ s₂, f x

theorem Finset.prod_subset_one_on_sdiff {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f g : α → β} [CommMonoid β] [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

theorem Finset.sum_subset_zero_on_sdiff {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f g : α → β} [AddCommMonoid β] [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

theorem Finset.prod_subset {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [CommMonoid β] (h : s₁ ⊆ s₂) (hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 1) : ∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x

theorem Finset.sum_subset {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [AddCommMonoid β] (h : s₁ ⊆ s₂) (hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 0) : ∑ x ∈ s₁, f x = ∑ x ∈ s₂, f x

@[simp]

theorem Finset.prod_disj_sum {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset α) (t : Finset γ) (f : α ⊕ γ → β) : ∏ x ∈ s.disjSum t, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)

@[simp]

theorem Finset.sum_disj_sum {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset α) (t : Finset γ) (f : α ⊕ γ → β) : ∑ x ∈ s.disjSum t, f x = ∑ x ∈ s, f (Sum.inl x) + ∑ x ∈ t, f (Sum.inr x)

theorem Finset.prod_sum_eq_prod_toLeft_mul_prod_toRight {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset (α ⊕ γ)) (f : α ⊕ γ → β) : ∏ x ∈ s, f x = (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x)

theorem Finset.sum_sum_eq_sum_toLeft_add_sum_toRight {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset (α ⊕ γ)) (f : α ⊕ γ → β) : ∑ x ∈ s, f x = ∑ x ∈ s.toLeft, f (Sum.inl x) + ∑ x ∈ s.toRight, f (Sum.inr x)

theorem Finset.prod_sumElim {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset α) (t : Finset γ) (f : α → β) (g : γ → β) : ∏ x ∈ s.disjSum t, Sum.elim f g x = (∏ x ∈ s, f x) * ∏ x ∈ t, g x

theorem Finset.sum_sumElim {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset α) (t : Finset γ) (f : α → β) (g : γ → β) : ∑ x ∈ s.disjSum t, Sum.elim f g x = ∑ x ∈ s, f x + ∑ x ∈ t, g x

@[deprecated Finset.prod_sumElim (since := "2025-02-20")]

theorem Finset.prod_sum_elim {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset α) (t : Finset γ) (f : α → β) (g : γ → β) : ∏ x ∈ s.disjSum t, Sum.elim f g x = (∏ x ∈ s, f x) * ∏ x ∈ t, g x

Alias of Finset.prod_sumElim.

@[deprecated Finset.sum_sumElim (since := "2025-02-20")]

theorem Finset.sum_sum_elim {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset α) (t : Finset γ) (f : α → β) (g : γ → β) : ∑ x ∈ s.disjSum t, Sum.elim f g x = ∑ x ∈ s, f x + ∑ x ∈ t, g x

Alias of Finset.sum_sumElim.

theorem Finset.prod_biUnion {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β} [CommMonoid β] [DecidableEq α] {s : Finset γ} {t : γ → Finset α} (hs : (↑s).PairwiseDisjoint t) : ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i

theorem Finset.sum_biUnion {α : Type u_3} {β : Type u_4} {γ : Type u_5} {f : α → β} [AddCommMonoid β] [DecidableEq α] {s : Finset γ} {t : γ → Finset α} (hs : (↑s).PairwiseDisjoint t) : ∑ x ∈ s.biUnion t, f x = ∑ x ∈ s, ∑ i ∈ t x, f i

theorem Finset.prod_of_injOn {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (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

theorem Finset.sum_of_injOn {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} {f : ι → α} {g : κ → α} (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

theorem Finset.prod_fiberwise_eq_prod_filter {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : ι → α) : ∏ j ∈ t, ∏ i ∈ {i ∈ s | g i = j}, f i = ∏ i ∈ {i ∈ s | g i ∈ t}, f i

theorem Finset.sum_fiberwise_eq_sum_filter {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : ι → α) : ∑ j ∈ t, ∑ i ∈ {i ∈ s | g i = j}, f i = ∑ i ∈ {i ∈ s | g i ∈ t}, f i

theorem Finset.prod_fiberwise_eq_prod_filter' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : κ → α) : ∏ j ∈ t, ∏ i ∈ {i ∈ s | g i = j}, f j = ∏ i ∈ {i ∈ s | g i ∈ t}, f (g i)

theorem Finset.sum_fiberwise_eq_sum_filter' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : κ → α) : ∑ j ∈ t, ∑ i ∈ {i ∈ s | g i = j}, f j = ∑ i ∈ {i ∈ s | g i ∈ t}, f (g i)

theorem Finset.prod_fiberwise_of_maps_to {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : ι → α) : ∏ j ∈ t, ∏ i ∈ {i ∈ s | g i = j}, f i = ∏ i ∈ s, f i

theorem Finset.sum_fiberwise_of_maps_to {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : ι → α) : ∑ j ∈ t, ∑ i ∈ {i ∈ s | g i = j}, f i = ∑ i ∈ s, f i

theorem Finset.prod_fiberwise_of_maps_to' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : κ → α) : ∏ j ∈ t, ∏ i ∈ {i ∈ s | g i = j}, f j = ∏ i ∈ s, f (g i)

theorem Finset.sum_fiberwise_of_maps_to' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] {s : Finset ι} {t : Finset κ} [DecidableEq κ] {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : κ → α) : ∑ j ∈ t, ∑ i ∈ {i ∈ s | g i = j}, f j = ∑ i ∈ s, f (g i)

theorem Finset.prod_fiberwise {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : ι → α) : ∏ j : κ, ∏ i ∈ {i ∈ s | g i = j}, f i = ∏ i ∈ s, f i

theorem Finset.sum_fiberwise {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : ι → α) : ∑ j : κ, ∑ i ∈ {i ∈ s | g i = j}, f i = ∑ i ∈ s, f i

theorem Finset.prod_fiberwise' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : κ → α) : ∏ j : κ, ∏ i ∈ {i ∈ s | g i = j}, f j = ∏ i ∈ s, f (g i)

theorem Finset.sum_fiberwise' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : κ → α) : ∑ j : κ, ∑ i ∈ {i ∈ s | g i = j}, f j = ∑ i ∈ s, f (g i)

@[simp]

theorem Finset.prod_diag {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (f : α × α → β) : ∏ i ∈ s.diag, f i = ∏ i ∈ s, f (i, i)

@[simp]

theorem Finset.sum_diag {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (f : α × α → β) : ∑ i ∈ s.diag, f i = ∑ i ∈ s, f (i, i)

theorem Finset.prod_image' {ι : Type u_1} {α : Type u_3} {β : Type u_4} {f : α → β} [CommMonoid β] [DecidableEq α] {s : Finset ι} {g : ι → α} (h : ι → β) (eq : ∀ i ∈ s, f (g i) = ∏ j ∈ {j ∈ s | g j = g i}, h j) : ∏ a ∈ image g s, f a = ∏ i ∈ s, h i

theorem Finset.sum_image' {ι : Type u_1} {α : Type u_3} {β : Type u_4} {f : α → β} [AddCommMonoid β] [DecidableEq α] {s : Finset ι} {g : ι → α} (h : ι → β) (eq : ∀ i ∈ s, f (g i) = ∑ j ∈ {j ∈ s | g j = g i}, h j) : ∑ a ∈ image g s, f a = ∑ i ∈ s, h i

theorem Finset.prod_mul_distrib {α : Type u_3} {β : Type u_4} {s : Finset α} {f g : α → β} [CommMonoid β] : ∏ x ∈ s, f x * g x = (∏ x ∈ s, f x) * ∏ x ∈ s, g x

theorem Finset.sum_add_distrib {α : Type u_3} {β : Type u_4} {s : Finset α} {f g : α → β} [AddCommMonoid β] : ∑ x ∈ s, (f x + g x) = ∑ x ∈ s, f x + ∑ x ∈ s, g x

theorem Finset.prod_mul_prod_comm {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] (f g h i : α → β) : (∏ a ∈ s, f a * g a) * ∏ a ∈ s, h a * i a = (∏ a ∈ s, f a * h a) * ∏ a ∈ s, g a * i a

theorem Finset.sum_add_sum_comm {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] (f g h i : α → β) : ∑ a ∈ s, (f a + g a) + ∑ a ∈ s, (h a + i a) = ∑ a ∈ s, (f a + h a) + ∑ a ∈ s, (g a + i a)

theorem Finset.prod_filter_of_ne {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] {p : α → Prop} [DecidablePred p] (hp : ∀ x ∈ s, f x ≠ 1 → p x) : ∏ x ∈ {x ∈ s | p x}, f x = ∏ x ∈ s, f x

theorem Finset.sum_filter_of_ne {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] {p : α → Prop} [DecidablePred p] (hp : ∀ x ∈ s, f x ≠ 0 → p x) : ∑ x ∈ {x ∈ s | p x}, f x = ∑ x ∈ s, f x

theorem Finset.prod_filter_ne_one {α : Type u_3} {β : Type u_4} {f : α → β} [CommMonoid β] (s : Finset α) [(x : α) → Decidable (f x ≠ 1)] : ∏ x ∈ {x ∈ s | f x ≠ 1}, f x = ∏ x ∈ s, f x

theorem Finset.sum_filter_ne_zero {α : Type u_3} {β : Type u_4} {f : α → β} [AddCommMonoid β] (s : Finset α) [(x : α) → Decidable (f x ≠ 0)] : ∑ x ∈ {x ∈ s | f x ≠ 0}, f x = ∑ x ∈ s, f x

theorem Finset.prod_filter {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] (p : α → Prop) [DecidablePred p] (f : α → β) : ∏ a ∈ {a ∈ s | p a}, f a = ∏ a ∈ s, if p a then f a else 1

theorem Finset.sum_filter {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] (p : α → Prop) [DecidablePred p] (f : α → β) : ∑ a ∈ {a ∈ s | p a}, f a = ∑ a ∈ s, if p a then f a else 0

theorem Finset.prod_eq_single_of_mem {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {f : α → β} (a : α) (h : a ∈ s) (h₀ : ∀ b ∈ s, b ≠ a → f b = 1) : ∏ x ∈ s, f x = f a

theorem Finset.sum_eq_single_of_mem {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {f : α → β} (a : α) (h : a ∈ s) (h₀ : ∀ b ∈ s, b ≠ a → f b = 0) : ∑ x ∈ s, f x = f a

theorem Finset.prod_eq_single {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {f : α → β} (a : α) (h₀ : ∀ b ∈ s, b ≠ a → f b = 1) (h₁ : a ∉ s → f a = 1) : ∏ x ∈ s, f x = f a

theorem Finset.sum_eq_single {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {f : α → β} (a : α) (h₀ : ∀ b ∈ s, b ≠ a → f b = 0) (h₁ : a ∉ s → f a = 0) : ∑ x ∈ s, f x = f a

theorem Finset.prod_union_eq_left {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [CommMonoid β] [DecidableEq α] (hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 1) : ∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₁, f a

theorem Finset.sum_union_eq_left {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [AddCommMonoid β] [DecidableEq α] (hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 0) : ∑ a ∈ s₁ ∪ s₂, f a = ∑ a ∈ s₁, f a

theorem Finset.prod_union_eq_right {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [CommMonoid β] [DecidableEq α] (hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1) : ∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₂, f a

theorem Finset.sum_union_eq_right {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [AddCommMonoid β] [DecidableEq α] (hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 0) : ∑ a ∈ s₁ ∪ s₂, f a = ∑ a ∈ s₂, f a

theorem Finset.prod_congr_of_eq_on_inter {α : Type u_6} {β : Type u_7} {s₁ s₂ : Finset α} {f g : α → β} [CommMonoid β] (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 : α → β 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.

theorem Finset.sum_congr_of_eq_on_inter {α : Type u_6} {β : Type u_7} {s₁ s₂ : Finset α} {f g : α → β} [AddCommMonoid β] (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 : α → β 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.

theorem Finset.prod_eq_mul_of_mem {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {f : α → β} (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

theorem Finset.sum_eq_add_of_mem {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {f : α → β} (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

theorem Finset.prod_eq_mul {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {f : α → β} (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

theorem Finset.sum_eq_add {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {f : α → β} (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

@[simp]

theorem Finset.prod_subtype_eq_prod_filter {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] (f : α → β) {p : α → Prop} [DecidablePred p] : ∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ {x ∈ s | p x}, f x

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

@[simp]

theorem Finset.sum_subtype_eq_sum_filter {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] (f : α → β) {p : α → Prop} [DecidablePred p] : ∑ x ∈ Finset.subtype p s, f ↑x = ∑ x ∈ {x ∈ s | p x}, f x

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

theorem Finset.prod_subtype_of_mem {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] (f : α → β) {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.

theorem Finset.sum_subtype_of_mem {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] (f : α → β) {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.

theorem Finset.prod_subtype_map_embedding {α : Type u_3} {β : Type u_4} [CommMonoid β] {p : α → Prop} {s : Finset { x : α // p x }} {f : { x : α // p x } → β} {g : α → β} (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.

theorem Finset.sum_subtype_map_embedding {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {p : α → Prop} {s : Finset { x : α // p x }} {f : { x : α // p x } → β} {g : α → β} (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.

theorem Finset.prod_coe_sort {α : Type u_3} {β : Type u_4} (s : Finset α) (f : α → β) [CommMonoid β] : ∏ i : { x : α // x ∈ s }, f ↑i = ∏ i ∈ s, f i

theorem Finset.sum_coe_sort {α : Type u_3} {β : Type u_4} (s : Finset α) (f : α → β) [AddCommMonoid β] : ∑ i : { x : α // x ∈ s }, f ↑i = ∑ i ∈ s, f i

theorem Finset.prod_finset_coe {α : Type u_3} {β : Type u_4} [CommMonoid β] (f : α → β) (s : Finset α) : ∏ i : ↑↑s, f ↑i = ∏ i ∈ s, f i

theorem Finset.sum_finset_coe {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (f : α → β) (s : Finset α) : ∑ i : ↑↑s, f ↑i = ∑ i ∈ s, f i

theorem Finset.prod_subtype {α : Type u_3} {β : Type u_4} [CommMonoid β] {p : α → Prop} {F : Fintype (Subtype p)} (s : Finset α) (h : ∀ (x : α), x ∈ s ↔ p x) (f : α → β) : ∏ a ∈ s, f a = ∏ a : Subtype p, f ↑a

theorem Finset.sum_subtype {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {p : α → Prop} {F : Fintype (Subtype p)} (s : Finset α) (h : ∀ (x : α), x ∈ s ↔ p x) (f : α → β) : ∑ a ∈ s, f a = ∑ a : Subtype p, f ↑a

theorem Finset.prod_set_coe {α : Type u_3} {β : Type u_4} {f : α → β} [CommMonoid β] (s : Set α) [Fintype ↑s] : ∏ i : ↑s, f ↑i = ∏ i ∈ s.toFinset, f i

theorem Finset.sum_set_coe {α : Type u_3} {β : Type u_4} {f : α → β} [AddCommMonoid β] (s : Set α) [Fintype ↑s] : ∑ i : ↑s, f ↑i = ∑ i ∈ s.toFinset, f i

theorem Finset.prod_congr_set {α : Type u_6} [CommMonoid α] {β : Type u_7} [Fintype β] (s : Set β) [DecidablePred fun (x : β) => x ∈ s] (f : β → α) (g : ↑s → α) (w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩) (w' : ∀ x ∉ s, f x = 1) : univ.prod f = univ.prod g

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.

theorem Finset.sum_congr_set {α : Type u_6} [AddCommMonoid α] {β : Type u_7} [Fintype β] (s : Set β) [DecidablePred fun (x : β) => x ∈ s] (f : β → α) (g : ↑s → α) (w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩) (w' : ∀ x ∉ s, f x = 0) : univ.sum f = univ.sum g

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.

theorem Finset.prod_extend_by_one {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) : (∏ i ∈ s, if i ∈ s then f i else 1) = ∏ i ∈ s, f i

theorem Finset.sum_extend_by_zero {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) : (∑ i ∈ s, if i ∈ s then f i else 0) = ∑ i ∈ s, f i

theorem Finset.prod_eq_prod_extend {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] (f : { x : α // x ∈ s } → β) : ∏ x : { x : α // x ∈ s }, f x = ∏ x ∈ s, Function.extend Subtype.val f 1 x

theorem Finset.sum_eq_sum_extend {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] (f : { x : α // x ∈ s } → β) : ∑ x : { x : α // x ∈ s }, f x = ∑ x ∈ s, Function.extend Subtype.val f 0 x

theorem Finset.prod_bij_ne_one {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β} (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

theorem Finset.sum_bij_ne_zero {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β} (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

theorem Finset.exists_ne_one_of_prod_ne_one {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] (h : ∏ x ∈ s, f x ≠ 1) : ∃ a ∈ s, f a ≠ 1

theorem Finset.exists_ne_zero_of_sum_ne_zero {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] (h : ∑ x ∈ s, f x ≠ 0) : ∃ a ∈ s, f a ≠ 0

theorem Finset.prod_range_succ_comm {β : Type u_4} [CommMonoid β] (f : ℕ → β) (n : ℕ) : ∏ x ∈ range (n + 1), f x = f n * ∏ x ∈ range n, f x

theorem Finset.sum_range_succ_comm {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) (n : ℕ) : ∑ x ∈ range (n + 1), f x = f n + ∑ x ∈ range n, f x

theorem Finset.prod_range_succ {β : Type u_4} [CommMonoid β] (f : ℕ → β) (n : ℕ) : ∏ x ∈ range (n + 1), f x = (∏ x ∈ range n, f x) * f n

theorem Finset.sum_range_succ {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) (n : ℕ) : ∑ x ∈ range (n + 1), f x = ∑ x ∈ range n, f x + f n

theorem Finset.prod_range_succ' {β : Type u_4} [CommMonoid β] (f : ℕ → β) (n : ℕ) : ∏ k ∈ range (n + 1), f k = (∏ k ∈ range n, f (k + 1)) * f 0

theorem Finset.sum_range_succ' {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) (n : ℕ) : ∑ k ∈ range (n + 1), f k = ∑ k ∈ range n, f (k + 1) + f 0

theorem Finset.eventually_constant_prod {β : Type u_4} [CommMonoid β] {u : ℕ → β} {N : ℕ} (hu : ∀ n ≥ N, u n = 1) {n : ℕ} (hn : N ≤ n) : ∏ k ∈ range n, u k = ∏ k ∈ range N, u k

theorem Finset.eventually_constant_sum {β : Type u_4} [AddCommMonoid β] {u : ℕ → β} {N : ℕ} (hu : ∀ n ≥ N, u n = 0) {n : ℕ} (hn : N ≤ n) : ∑ k ∈ range n, u k = ∑ k ∈ range N, u k

theorem Finset.prod_range_add {β : Type u_4} [CommMonoid β] (f : ℕ → β) (n m : ℕ) : ∏ x ∈ range (n + m), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range m, f (n + x)

theorem Finset.sum_range_add {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) (n m : ℕ) : ∑ x ∈ range (n + m), f x = ∑ x ∈ range n, f x + ∑ x ∈ range m, f (n + x)

theorem Finset.prod_range_add_div_prod_range {α : Type u_6} [CommGroup α] (f : ℕ → α) (n m : ℕ) : (∏ k ∈ range (n + m), f k) / ∏ k ∈ range n, f k = ∏ k ∈ range m, f (n + k)

theorem Finset.sum_range_add_sub_sum_range {α : Type u_6} [AddCommGroup α] (f : ℕ → α) (n m : ℕ) : ∑ k ∈ range (n + m), f k - ∑ k ∈ range n, f k = ∑ k ∈ range m, f (n + k)

theorem Finset.prod_range_one {β : Type u_4} [CommMonoid β] (f : ℕ → β) : ∏ k ∈ range 1, f k = f 0

theorem Finset.sum_range_one {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) : ∑ k ∈ range 1, f k = f 0

theorem Finset.prod_list_map_count {α : Type u_3} [DecidableEq α] (l : List α) {M : Type u_6} [CommMonoid M] (f : α → M) : (List.map f l).prod = ∏ m ∈ l.toFinset, f m ^ List.count m l

theorem Finset.sum_list_map_count {α : Type u_3} [DecidableEq α] (l : List α) {M : Type u_6} [AddCommMonoid M] (f : α → M) : (List.map f l).sum = ∑ m ∈ l.toFinset, List.count m l • f m

theorem Finset.prod_list_count {α : Type u_3} [DecidableEq α] [CommMonoid α] (s : List α) : s.prod = ∏ m ∈ s.toFinset, m ^ List.count m s

theorem Finset.sum_list_count {α : Type u_3} [DecidableEq α] [AddCommMonoid α] (s : List α) : s.sum = ∑ m ∈ s.toFinset, List.count m s • m

theorem Finset.prod_list_count_of_subset {α : Type u_3} [DecidableEq α] [CommMonoid α] (m : List α) (s : Finset α) (hs : m.toFinset ⊆ s) : m.prod = ∏ i ∈ s, i ^ List.count i m

theorem Finset.sum_list_count_of_subset {α : Type u_3} [DecidableEq α] [AddCommMonoid α] (m : List α) (s : Finset α) (hs : m.toFinset ⊆ s) : m.sum = ∑ i ∈ s, List.count i m • i

theorem Finset.prod_multiset_map_count {α : Type u_3} [DecidableEq α] (s : Multiset α) {M : Type u_6} [CommMonoid M] (f : α → M) : (Multiset.map f s).prod = ∏ m ∈ s.toFinset, f m ^ Multiset.count m s

theorem Finset.sum_multiset_map_count {α : Type u_3} [DecidableEq α] (s : Multiset α) {M : Type u_6} [AddCommMonoid M] (f : α → M) : (Multiset.map f s).sum = ∑ m ∈ s.toFinset, Multiset.count m s • f m

theorem Finset.prod_multiset_count {α : Type u_3} [DecidableEq α] [CommMonoid α] (s : Multiset α) : s.prod = ∏ m ∈ s.toFinset, m ^ Multiset.count m s

theorem Finset.sum_multiset_count {α : Type u_3} [DecidableEq α] [AddCommMonoid α] (s : Multiset α) : s.sum = ∑ m ∈ s.toFinset, Multiset.count m s • m

theorem Finset.prod_multiset_count_of_subset {α : Type u_3} [DecidableEq α] [CommMonoid α] (m : Multiset α) (s : Finset α) (hs : m.toFinset ⊆ s) : m.prod = ∏ i ∈ s, i ^ Multiset.count i m

theorem Finset.sum_multiset_count_of_subset {α : Type u_3} [DecidableEq α] [AddCommMonoid α] (m : Multiset α) (s : Finset α) (hs : m.toFinset ⊆ s) : m.sum = ∑ i ∈ s, Multiset.count i m • i

theorem Finset.prod_range_induction {β : Type u_4} [CommMonoid β] (f s : ℕ → β) (base : s 0 = 1) (step : ∀ (n : ℕ), s (n + 1) = s n * f n) (n : ℕ) : ∏ 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.

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

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

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

theorem Finset.prod_range_div {M : Type u_6} [CommGroup M] (f : ℕ → M) (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.

theorem Finset.sum_range_sub {M : Type u_6} [AddCommGroup M] (f : ℕ → M) (n : ℕ) : ∑ i ∈ 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.prod_range_div' {M : Type u_6} [CommGroup M] (f : ℕ → M) (n : ℕ) : ∏ i ∈ range n, f i / f (i + 1) = f 0 / f n

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

theorem Finset.eq_prod_range_div {M : Type u_6} [CommGroup M] (f : ℕ → M) (n : ℕ) : f n = f 0 * ∏ i ∈ range n, f (i + 1) / f i

theorem Finset.eq_sum_range_sub {M : Type u_6} [AddCommGroup M] (f : ℕ → M) (n : ℕ) : f n = f 0 + ∑ i ∈ range n, (f (i + 1) - f i)

theorem Finset.eq_prod_range_div' {M : Type u_6} [CommGroup M] (f : ℕ → M) (n : ℕ) : f n = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1)

theorem Finset.eq_sum_range_sub' {M : Type u_6} [AddCommGroup M] (f : ℕ → M) (n : ℕ) : f n = ∑ i ∈ range (n + 1), if i = 0 then f 0 else f i - f (i - 1)

theorem Finset.sum_range_tsub {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [Sub α] [OrderedSub α] [AddLeftMono α] [AddLeftReflectLE α] [ExistsAddOfLE α] {f : ℕ → α} (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.

theorem Finset.sum_tsub_distrib {ι : Type u_1} {α : Type u_3} [AddCommMonoid α] [PartialOrder α] [ExistsAddOfLE α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [Sub α] [OrderedSub α] (s : Finset ι) {f g : ι → α} (hfg : ∀ x ∈ s, g x ≤ f x) : ∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x - ∑ x ∈ s, g x

@[simp]

theorem Finset.prod_const {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] (b : β) : ∏ _x ∈ s, b = b ^ s.card

@[simp]

theorem Finset.sum_const {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] (b : β) : ∑ _x ∈ s, b = s.card • b

theorem Finset.prod_eq_pow_card {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] {b : β} (hf : ∀ a ∈ s, f a = b) : ∏ a ∈ s, f a = b ^ s.card

theorem Finset.sum_eq_card_nsmul {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] {b : β} (hf : ∀ a ∈ s, f a = b) : ∑ a ∈ s, f a = s.card • b

theorem Finset.pow_card_mul_prod {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] {b : β} : b ^ s.card * ∏ a ∈ s, f a = ∏ a ∈ s, b * f a

theorem Finset.card_nsmul_add_sum {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] {b : β} : s.card • b + ∑ a ∈ s, f a = ∑ a ∈ s, (b + f a)

theorem Finset.prod_mul_pow_card {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] {b : β} : (∏ a ∈ s, f a) * b ^ s.card = ∏ a ∈ s, f a * b

theorem Finset.sum_add_card_nsmul {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] {b : β} : ∑ a ∈ s, f a + s.card • b = ∑ a ∈ s, (f a + b)

theorem Finset.pow_eq_prod_const {β : Type u_4} [CommMonoid β] (b : β) (n : ℕ) : b ^ n = ∏ _k ∈ range n, b

theorem Finset.nsmul_eq_sum_const {β : Type u_4} [AddCommMonoid β] (b : β) (n : ℕ) : n • b = ∑ _k ∈ range n, b

theorem Finset.prod_pow_eq_pow_sum {ι : Type u_1} {β : Type u_4} [CommMonoid β] (s : Finset ι) (f : ι → ℕ) (a : β) : ∏ i ∈ s, a ^ f i = a ^ ∑ i ∈ s, f i

theorem Finset.sum_nsmul_assoc {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] (s : Finset ι) (f : ι → ℕ) (a : β) : ∑ i ∈ s, f i • a = (∑ i ∈ s, f i) • a

theorem Finset.prod_flip {β : Type u_4} [CommMonoid β] {n : ℕ} (f : ℕ → β) : ∏ r ∈ range (n + 1), f (n - r) = ∏ k ∈ range (n + 1), f k

theorem Finset.sum_flip {β : Type u_4} [AddCommMonoid β] {n : ℕ} (f : ℕ → β) : ∑ r ∈ range (n + 1), f (n - r) = ∑ k ∈ range (n + 1), f k

theorem Finset.prod_involution {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] (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.

theorem Finset.sum_involution {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] (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.

theorem Finset.prod_ninvolution {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] (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.

theorem Finset.sum_ninvolution {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] (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.

theorem Finset.prod_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [CommMonoid β] [DecidableEq γ] (f : γ → β) (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.

theorem Finset.sum_comp {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [AddCommMonoid β] [DecidableEq γ] (f : γ → β) (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.

theorem Finset.prod_partition {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] (R : Setoid α) [DecidableRel ⇑R] : ∏ x ∈ s, f x = ∏ xbar ∈ image (Quotient.mk R) s, ∏ y ∈ {y ∈ s | ⟦y⟧ = xbar}, f y

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

theorem Finset.sum_partition {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] (R : Setoid α) [DecidableRel ⇑R] : ∑ x ∈ s, f x = ∑ xbar ∈ image (Quotient.mk R) s, ∑ y ∈ {y ∈ s | ⟦y⟧ = xbar}, f y

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

theorem Finset.prod_cancels_of_partition_cancels {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] (R : Setoid α) [DecidableRel ⇑R] (h : ∀ x ∈ s, ∏ a ∈ {a ∈ s | 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.

theorem Finset.sum_cancels_of_partition_cancels {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] (R : Setoid α) [DecidableRel ⇑R] (h : ∀ x ∈ s, ∑ a ∈ {a ∈ s | 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.

theorem Finset.eq_of_card_le_one_of_prod_eq {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} (hc : s.card ≤ 1) {f : α → β} {b : β} (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.

theorem Finset.eq_of_card_le_one_of_sum_eq {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} (hc : s.card ≤ 1) {f : α → β} {b : β} (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.

theorem Finset.mul_prod_erase {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) {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.

theorem Finset.add_sum_erase {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) {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.

theorem Finset.prod_erase_mul {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) {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.

theorem Finset.sum_erase_add {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) {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.

theorem Finset.prod_erase {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) {f : α → β} {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.

theorem Finset.sum_erase {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) {f : α → β} {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.

theorem Finset.prod_erase_lt_of_one_lt {α : Type u_3} {γ : Type u_6} [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

theorem Finset.sum_erase_lt_of_pos {α : Type u_3} {γ : Type u_6} [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

theorem Finset.eq_one_of_prod_eq_one {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {f : α → β} {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.

theorem Finset.eq_zero_of_sum_eq_zero {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {f : α → β} {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.

theorem Finset.prod_dvd_prod_of_dvd {α : Type u_3} {β : Type u_4} [CommMonoid β] {S : Finset α} (g1 g2 : α → β) (h : ∀ a ∈ S, g1 a ∣ g2 a) : S.prod g1 ∣ S.prod g2

theorem Finset.prod_mul_eq_prod_mul_of_exists {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {f : α → β} {b₁ b₂ : β} (a : α) (ha : a ∈ s) (h : f a * b₁ = f a * b₂) : (∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂

theorem Finset.sum_add_eq_sum_add_of_exists {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {f : α → β} {b₁ b₂ : β} (a : α) (ha : a ∈ s) (h : f a + b₁ = f a + b₂) : ∑ a ∈ s, f a + b₁ = ∑ a ∈ s, f a + b₂

theorem Finset.prod_sdiff_eq_prod_sdiff_iff {ι : Type u_1} {α : Type u_3} [DecidableEq ι] [CancelCommMonoid α] {s t : Finset ι} {f : ι → α} : ∏ i ∈ s \ t, f i = ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i = ∏ i ∈ t, f i

theorem Finset.sum_sdiff_eq_sum_sdiff_iff {ι : Type u_1} {α : Type u_3} [DecidableEq ι] [AddCancelCommMonoid α] {s t : Finset ι} {f : ι → α} : ∑ i ∈ s \ t, f i = ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i = ∑ i ∈ t, f i

theorem Finset.prod_sdiff_ne_prod_sdiff_iff {ι : Type u_1} {α : Type u_3} [DecidableEq ι] [CancelCommMonoid α] {s t : Finset ι} {f : ι → α} : ∏ i ∈ s \ t, f i ≠ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≠ ∏ i ∈ t, f i

theorem Finset.sum_sdiff_ne_sum_sdiff_iff {ι : Type u_1} {α : Type u_3} [DecidableEq ι] [AddCancelCommMonoid α] {s t : Finset ι} {f : ι → α} : ∑ i ∈ s \ t, f i ≠ ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i ≠ ∑ i ∈ t, f i

theorem Finset.card_eq_sum_ones {α : Type u_3} (s : Finset α) : s.card = ∑ x ∈ s, 1

theorem Finset.sum_const_nat {α : Type u_3} {s : Finset α} {m : ℕ} {f : α → ℕ} (h₁ : ∀ x ∈ s, f x = m) : ∑ x ∈ s, f x = s.card * m

theorem Finset.sum_card_fiberwise_eq_card_filter {ι : Type u_1} {κ : Type u_6} [DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ) : ∑ j ∈ t, {i ∈ s | g i = j}.card = {i ∈ s | g i ∈ t}.card

@[simp]

theorem Finset.prod_sdiff_eq_div {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [CommGroup β] [DecidableEq α] (h : s₁ ⊆ s₂) : ∏ x ∈ s₂ \ s₁, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x

@[simp]

theorem Finset.sum_sdiff_eq_sub {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [AddCommGroup β] [DecidableEq α] (h : s₁ ⊆ s₂) : ∑ x ∈ s₂ \ s₁, f x = ∑ x ∈ s₂, f x - ∑ x ∈ s₁, f x

theorem Finset.prod_sdiff_div_prod_sdiff {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [CommGroup β] [DecidableEq α] : (∏ x ∈ s₂ \ s₁, f x) / ∏ x ∈ s₁ \ s₂, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x

theorem Finset.sum_sdiff_sub_sum_sdiff {α : Type u_3} {β : Type u_4} {s₁ s₂ : Finset α} {f : α → β} [AddCommGroup β] [DecidableEq α] : ∑ x ∈ s₂ \ s₁, f x - ∑ x ∈ s₁ \ s₂, f x = ∑ x ∈ s₂, f x - ∑ x ∈ s₁, f x

@[simp]

theorem Finset.prod_erase_eq_div {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommGroup β] [DecidableEq α] {a : α} (h : a ∈ s) : ∏ x ∈ s.erase a, f x = (∏ x ∈ s, f x) / f a

@[simp]

theorem Finset.sum_erase_eq_sub {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommGroup β] [DecidableEq α] {a : α} (h : a ∈ s) : ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x - f a

@[simp]

theorem Finset.card_disjiUnion {α : Type u_3} {β : Type u_4} (s : Finset α) (t : α → Finset β) (h : (↑s).PairwiseDisjoint t) : (s.disjiUnion t h).card = ∑ a ∈ s, (t a).card

theorem Finset.card_biUnion {α : Type u_3} {β : Type u_4} {s : Finset α} [DecidableEq β] {t : α → Finset β} (h : (↑s).PairwiseDisjoint t) : (s.biUnion t).card = ∑ u ∈ s, (t u).card

theorem Finset.card_biUnion_le {α : Type u_3} {β : Type u_4} [DecidableEq β] {s : Finset α} {t : α → Finset β} : (s.biUnion t).card ≤ ∑ a ∈ s, (t a).card

theorem Finset.card_eq_sum_card_fiberwise {α : Type u_3} {β : Type u_4} [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β} (H : Set.MapsTo f ↑s ↑t) : s.card = ∑ b ∈ t, {a ∈ s | f a = b}.card

theorem Finset.card_eq_sum_card_image {α : Type u_3} {β : Type u_4} [DecidableEq β] (f : α → β) (s : Finset α) : s.card = ∑ b ∈ image f s, {a ∈ s | f a = b}.card

theorem Finset.mem_sum {α : Type u_3} {β : Type u_4} {f : α → Multiset β} (s : Finset α) (b : β) : b ∈ ∑ x ∈ s, f x ↔ ∃ a ∈ s, b ∈ f a

theorem Finset.prod_unique_nonempty {α : Type u_6} {β : Type u_7} [CommMonoid β] [Unique α] (s : Finset α) (f : α → β) (h : s.Nonempty) : ∏ x ∈ s, f x = f default

theorem Finset.sum_unique_nonempty {α : Type u_6} {β : Type u_7} [AddCommMonoid β] [Unique α] (s : Finset α) (f : α → β) (h : s.Nonempty) : ∑ x ∈ s, f x = f default

theorem Finset.prod_filter_of_pairwise_eq_one {α : Type u_6} {β : Type u_7} {ι : Type u_8} [DecidableEq α] [CommMonoid β] {f : ι → α} {g : α → β} {n : ι} {I : Finset ι} (hn : n ∈ I) (hf : (↑I).Pairwise fun (i j : ι) => f i = f j → g (f i) = 1) : ∏ j ∈ {j ∈ I | f j = f n}, g (f j) = g (f n)

theorem Finset.sum_filter_of_pairwise_eq_zero {α : Type u_6} {β : Type u_7} {ι : Type u_8} [DecidableEq α] [AddCommMonoid β] {f : ι → α} {g : α → β} {n : ι} {I : Finset ι} (hn : n ∈ I) (hf : (↑I).Pairwise fun (i j : ι) => f i = f j → g (f i) = 0) : ∑ j ∈ {j ∈ I | f j = f n}, g (f j) = g (f n)

@[simp]

theorem Finset.prod_image_of_pairwise_eq_one {α : Type u_6} {β : Type u_7} {ι : Type u_8} [DecidableEq α] [CommMonoid β] {f : ι → α} {g : α → β} {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.

@[simp]

theorem Finset.sum_image_of_pairwise_eq_zero {α : Type u_6} {β : Type u_7} {ι : Type u_8} [DecidableEq α] [AddCommMonoid β] {f : ι → α} {g : α → β} {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.

@[simp]

theorem Finset.prod_image_of_disjoint {α : Type u_6} {β : Type u_7} {ι : Type u_8} [DecidableEq α] [CommMonoid β] [PartialOrder α] [OrderBot α] {f : ι → α} {g : α → β} (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.

@[simp]

theorem Finset.sum_image_of_disjoint {α : Type u_6} {β : Type u_7} {ι : Type u_8} [DecidableEq α] [AddCommMonoid β] [PartialOrder α] [OrderBot α] {f : ι → α} {g : α → β} (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.

theorem Fintype.prod_of_injective {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommMonoid α] (e : ι → κ) (he : Function.Injective e) (f : ι → α) (g : κ → α) (h' : ∀ i ∉ Set.range e, g i = 1) (h : ∀ (i : ι), f i = g (e i)) : ∏ i : ι, f i = ∏ j : κ, g j

theorem Fintype.sum_of_injective {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] (e : ι → κ) (he : Function.Injective e) (f : ι → α) (g : κ → α) (h' : ∀ i ∉ Set.range e, g i = 0) (h : ∀ (i : ι), f i = g (e i)) : ∑ i : ι, f i = ∑ j : κ, g j

theorem Fintype.prod_fiberwise {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommMonoid α] [DecidableEq κ] (g : ι → κ) (f : ι → α) : ∏ j : κ, ∏ i : { i : ι // g i = j }, f ↑i = ∏ i : ι, f i

theorem Fintype.sum_fiberwise {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] [DecidableEq κ] (g : ι → κ) (f : ι → α) : ∑ j : κ, ∑ i : { i : ι // g i = j }, f ↑i = ∑ i : ι, f i

theorem Fintype.prod_fiberwise' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [CommMonoid α] [DecidableEq κ] (g : ι → κ) (f : κ → α) : ∏ j : κ, ∏ _i : { i : ι // g i = j }, f j = ∏ i : ι, f (g i)

theorem Fintype.sum_fiberwise' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [Fintype ι] [Fintype κ] [AddCommMonoid α] [DecidableEq κ] (g : ι → κ) (f : κ → α) : ∑ j : κ, ∑ _i : { i : ι // g i = j }, f j = ∑ i : ι, f (g i)

theorem Fintype.prod_unique {α : Type u_9} {β : Type u_10} [CommMonoid β] [Unique α] [Fintype α] (f : α → β) : ∏ x : α, f x = f default

theorem Fintype.sum_unique {α : Type u_9} {β : Type u_10} [AddCommMonoid β] [Unique α] [Fintype α] (f : α → β) : ∑ x : α, f x = f default

theorem Fintype.prod_subsingleton {α : Type u_9} {β : Type u_10} [CommMonoid β] [Subsingleton α] [Fintype α] (f : α → β) (a : α) : ∏ x : α, f x = f a

theorem Fintype.sum_subsingleton {α : Type u_9} {β : Type u_10} [AddCommMonoid β] [Subsingleton α] [Fintype α] (f : α → β) (a : α) : ∑ x : α, f x = f a

theorem Fintype.prod_Prop {β : Type u_9} [CommMonoid β] (f : Prop → β) : ∏ p : Prop, f p = f True * f False

theorem Fintype.sum_Prop {β : Type u_9} [AddCommMonoid β] (f : Prop → β) : ∑ p : Prop, f p = f True + f False

theorem Fintype.prod_subtype_mul_prod_subtype {α : Type u_9} {β : Type u_10} [Fintype α] [CommMonoid β] (p : α → Prop) (f : α → β) [DecidablePred p] : (∏ i : { x : α // p x }, f ↑i) * ∏ i : { x : α // ¬p x }, f ↑i = ∏ i : α, f i

theorem Fintype.sum_subtype_add_sum_subtype {α : Type u_9} {β : Type u_10} [Fintype α] [AddCommMonoid β] (p : α → Prop) (f : α → β) [DecidablePred p] : ∑ i : { x : α // p x }, f ↑i + ∑ i : { x : α // ¬p x }, f ↑i = ∑ i : α, f i

theorem Fintype.prod_subset {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] {s : Finset ι} {f : ι → α} (h : ∀ (i : ι), f i ≠ 1 → i ∈ s) : ∏ i ∈ s, f i = ∏ i : ι, f i

theorem Fintype.sum_subset {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] {s : Finset ι} {f : ι → α} (h : ∀ (i : ι), f i ≠ 0 → i ∈ s) : ∑ i ∈ s, f i = ∑ i : ι, f i

theorem List.prod_toFinset {α : Type u_3} {M : Type u_6} [DecidableEq α] [CommMonoid M] (f : α → M) {l : List α} (_hl : l.Nodup) : l.toFinset.prod f = (map f l).prod

theorem List.sum_toFinset {α : Type u_3} {M : Type u_6} [DecidableEq α] [AddCommMonoid M] (f : α → M) {l : List α} (_hl : l.Nodup) : l.toFinset.sum f = (map f l).sum

@[simp]

theorem List.sum_toFinset_count_eq_length {α : Type u_3} [DecidableEq α] (l : List α) : ∑ a ∈ l.toFinset, count a l = l.length

@[simp]

theorem Multiset.mem_sum {ι : Type u_1} {α : Type u_3} {a : α} {s : Finset ι} {m : ι → Multiset α} : a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i

theorem Multiset.toFinset_sum_count_eq {α : Type u_3} [DecidableEq α] (s : Multiset α) : ∑ a ∈ s.toFinset, count a s = s.card

@[simp]

theorem Multiset.sum_count_eq_card {α : Type u_3} [DecidableEq α] {s : Finset α} {m : Multiset α} (hms : ∀ a ∈ m, a ∈ s) : ∑ a ∈ s, count a m = m.card

@[simp]

theorem Multiset.toFinset_sum_count_nsmul_eq {α : Type u_3} [DecidableEq α] (s : Multiset α) : ∑ a ∈ s.toFinset, count a s • {a} = s

theorem Multiset.exists_smul_of_dvd_count {α : Type u_3} [DecidableEq α] (s : Multiset α) {k : ℕ} (h : ∀ a ∈ s, k ∣ count a s) : ∃ (u : Multiset α), s = k • u

theorem Multiset.prod_sum {α : Type u_6} {ι : Type u_7} [CommMonoid α] (f : ι → Multiset α) (s : Finset ι) : (∑ x ∈ s, f x).prod = ∏ x ∈ s, (f x).prod

theorem Multiset.sum_sum {α : Type u_6} {ι : Type u_7} [AddCommMonoid α] (f : ι → Multiset α) (s : Finset ι) : (∑ x ∈ s, f x).sum = ∑ x ∈ s, (f x).sum

@[simp]

theorem IsUnit.prod_iff {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] : IsUnit (∏ a ∈ s, f a) ↔ ∀ a ∈ s, IsUnit (f a)

@[simp]

theorem IsAddUnit.sum_iff {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] : IsAddUnit (∑ a ∈ s, f a) ↔ ∀ a ∈ s, IsAddUnit (f a)

theorem IsUnit.prod_univ_iff {α : Type u_3} {β : Type u_4} {f : α → β} [Fintype α] [CommMonoid β] : IsUnit (∏ a : α, f a) ↔ ∀ (a : α), IsUnit (f a)

theorem IsAddUnit.sum_univ_iff {α : Type u_3} {β : Type u_4} {f : α → β} [Fintype α] [AddCommMonoid β] : IsAddUnit (∑ a : α, f a) ↔ ∀ (a : α), IsAddUnit (f a)

theorem nat_abs_sum_le {ι : Type u_6} (s : Finset ι) (f : ι → ℤ) : (∑ i ∈ s, f i).natAbs ≤ ∑ i ∈ s, (f i).natAbs