Big operators

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

Notation

We introduce the following notation.

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

• ∏ x ∈ s, f x is notation for Finset.prod s f (assuming β is a CommMonoid)
• ∑ x ∈ s, f x is notation for Finset.sum s f (assuming β is an AddCommMonoid)
• ∏ x, f x is notation for Finset.prod Finset.univ f (assuming α is a Fintype and β is a CommMonoid)
• ∑ x, f x is notation for Finset.sum Finset.univ f (assuming α is a Fintype and β is an AddCommMonoid)

Implementation Notes

The first arguments in all definitions and lemmas is the codomain of the function of the big operator. This is necessary for the heuristic in @[to_additive]. See the documentation of to_additive.attr for more information.

theorem Finset.prod_eq_fold {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : α → β) : ∏ x ∈ s, f x = Finset.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 = Finset.fold (fun (x1 x2 : β) => x1 + x2) 0 f s

theorem MonoidHom.coe_finset_prod {α : Type u_3} {β : Type u_4} {γ : Type u_5} [MulOneClass β] [CommMonoid γ] (f : α → β →* γ) (s : Finset α) : ⇑(∏ x ∈ s, f x) = ∏ x ∈ s, ⇑(f x)

theorem AddMonoidHom.coe_finset_sum {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddZeroClass β] [AddCommMonoid γ] (f : α → β →+ γ) (s : Finset α) : ⇑(∑ x ∈ s, f x) = ∑ x ∈ s, ⇑(f x)

@[simp]

theorem MonoidHom.finset_prod_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [MulOneClass β] [CommMonoid γ] (f : α → β →* γ) (s : Finset α) (b : β) : (∏ x ∈ s, f x) b = ∏ x ∈ s, (f x) b

See also Finset.prod_apply, with the same conclusion but with the weaker hypothesis f : α → β → γ

@[simp]

theorem AddMonoidHom.finset_sum_apply {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddZeroClass β] [AddCommMonoid γ] (f : α → β →+ γ) (s : Finset α) (b : β) : (∑ x ∈ s, f x) b = ∑ x ∈ s, (f x) b

See also Finset.sum_apply, with the same conclusion but with the weaker hypothesis f : α → β → γ

@[simp]

theorem Finset.prod_cons {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} {f : α → β} [CommMonoid β] (h : a ∉ s) : ∏ x ∈ Finset.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 ∈ Finset.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 ∈ Finset.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 ∈ Finset.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 ∈ Finset.filter (fun (x : α) => p x) s, f x) * ∏ x ∈ Finset.filter (fun (x : α) => ¬p x) s, 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 ∈ Finset.filter (fun (x : α) => p x) s, f x + ∑ x ∈ Finset.filter (fun (x : α) => ¬p x) s, 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 ∈ Finset.filter (fun (x : α) => ¬p x) s, f x) * ∏ x ∈ Finset.filter p s, 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 ∈ Finset.filter (fun (x : α) => ¬p x) s, f x + ∑ x ∈ Finset.filter p s, 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 ∈ Finset.filter (fun (x : α) => Xor' (p x) (q x)) s, f x = (∏ x ∈ Finset.filter (fun (x : α) => p x ∧ ¬q x) s, f x) * ∏ x ∈ Finset.filter (fun (x : α) => q x ∧ ¬p x) s, 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 ∈ Finset.filter (fun (x : α) => Xor' (p x) (q x)) s, f x = ∑ x ∈ Finset.filter (fun (x : α) => p x ∧ ¬q x) s, f x + ∑ x ∈ Finset.filter (fun (x : α) => q x ∧ ¬p x) s, f x

theorem Finset.prod_powerset_insert {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} [CommMonoid β] [DecidableEq α] (ha : a ∉ s) (f : Finset α → β) : ∏ t ∈ (insert a s).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t)

A product over all subsets of s ∪ {x} is obtained by multiplying the product over all subsets of s, and over all subsets of s to which one adds x.

theorem Finset.sum_powerset_insert {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} [AddCommMonoid β] [DecidableEq α] (ha : a ∉ s) (f : Finset α → β) : ∑ t ∈ (insert a s).powerset, f t = ∑ t ∈ s.powerset, f t + ∑ t ∈ s.powerset, f (insert a t)

A sum over all subsets of s ∪ {x} is obtained by summing the sum over all subsets of s, and over all subsets of s to which one adds x.

theorem Finset.prod_powerset_cons {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} [CommMonoid β] (ha : a ∉ s) (f : Finset α → β) : ∏ t ∈ (Finset.cons a s ha).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset.attach, f (Finset.cons a ↑t ⋯)

A product over all subsets of s ∪ {x} is obtained by multiplying the product over all subsets of s, and over all subsets of s to which one adds x.

theorem Finset.sum_powerset_cons {α : Type u_3} {β : Type u_4} {s : Finset α} {a : α} [AddCommMonoid β] (ha : a ∉ s) (f : Finset α → β) : ∑ t ∈ (Finset.cons a s ha).powerset, f t = ∑ t ∈ s.powerset, f t + ∑ t ∈ s.powerset.attach, f (Finset.cons a ↑t ⋯)

A sum over all subsets of s ∪ {x} is obtained by summing the sum over all subsets of s, and over all subsets of s to which one adds x.

theorem Finset.prod_powerset {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : Finset α → β) : ∏ t ∈ s.powerset, f t = ∏ j ∈ Finset.range (s.card + 1), ∏ t ∈ Finset.powersetCard j s, f t

A product over powerset s is equal to the double product over sets of subsets of s with #s = k, for k = 1, ..., #s.

theorem Finset.sum_powerset {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : Finset α → β) : ∑ t ∈ s.powerset, f t = ∑ j ∈ Finset.range (s.card + 1), ∑ t ∈ Finset.powersetCard j s, f t

A sum over powerset s is equal to the double sum over sets of subsets of s with #s = k, for k = 1, ..., #s

theorem IsCompl.prod_mul_prod {α : Type u_3} {β : Type u_4} [Fintype α] [CommMonoid β] {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} [Fintype α] [AddCommMonoid β] {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_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

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

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_sigma {α : Type u_3} {β : Type u_4} [CommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : Sigma σ → β) : ∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩

The product over a sigma type equals the product of the fiberwise products. For rewriting in the reverse direction, use Finset.prod_sigma'.

theorem Finset.sum_sigma {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : Sigma σ → β) : ∑ x ∈ s.sigma t, f x = ∑ a ∈ s, ∑ s ∈ t a, f ⟨a, s⟩

The sum over a sigma type equals the sum of the fiberwise sums. For rewriting in the reverse direction, use Finset.sum_sigma'

theorem Finset.prod_sigma' {α : Type u_3} {β : Type u_4} [CommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : (a : α) → σ a → β) : ∏ a ∈ s, ∏ s ∈ t a, f a s = ∏ x ∈ s.sigma t, f x.fst x.snd

The product over a sigma type equals the product of the fiberwise products. For rewriting in the reverse direction, use Finset.prod_sigma.

theorem Finset.sum_sigma' {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : (a : α) → σ a → β) : ∑ a ∈ s, ∑ s ∈ t a, f a s = ∑ x ∈ s.sigma t, f x.fst x.snd

The sum over a sigma type equals the sum of the fiberwise sums. For rewriting in the reverse direction, use Finset.sum_sigma

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 ∈ Finset.filter (fun (i : ι) => g i = j) s, f i = ∏ i ∈ Finset.filter (fun (i : ι) => g i ∈ t) s, 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 ∈ Finset.filter (fun (i : ι) => g i = j) s, f i = ∑ i ∈ Finset.filter (fun (i : ι) => g i ∈ t) s, 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 ∈ Finset.filter (fun (i : ι) => g i = j) s, f j = ∏ i ∈ Finset.filter (fun (i : ι) => g i ∈ t) s, 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 ∈ Finset.filter (fun (i : ι) => g i = j) s, f j = ∑ i ∈ Finset.filter (fun (i : ι) => g i ∈ t) s, 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 ∈ Finset.filter (fun (i : ι) => g i = j) s, 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 ∈ Finset.filter (fun (i : ι) => g i = j) s, 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 ∈ Finset.filter (fun (i : ι) => g i = j) s, 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 ∈ Finset.filter (fun (i : ι) => g i = j) s, 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 ∈ Finset.filter (fun (i : ι) => g i = j) s, 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 ∈ Finset.filter (fun (i : ι) => g i = j) s, 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 ∈ Finset.filter (fun (i : ι) => g i = j) s, 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 ∈ Finset.filter (fun (i : ι) => g i = j) s, f j = ∑ i ∈ s, f (g i)

theorem Finset.prod_univ_pi {ι : Type u_1} {β : Type u_4} [CommMonoid β] [DecidableEq ι] [Fintype ι] {κ : ι → Type u_6} (t : (i : ι) → Finset (κ i)) (f : ((i : ι) → i ∈ Finset.univ → κ i) → β) : ∏ x ∈ Finset.univ.pi t, f x = ∏ x ∈ Fintype.piFinset t, f fun (a : ι) (x_1 : a ∈ Finset.univ) => x a

Taking a product over univ.pi t is the same as taking the product over Fintype.piFinset t. univ.pi t and Fintype.piFinset t are essentially the same Finset, but differ in the type of their element, univ.pi t is a Finset (Π a ∈ univ, t a) and Fintype.piFinset t is a Finset (Π a, t a).

theorem Finset.sum_univ_pi {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] [DecidableEq ι] [Fintype ι] {κ : ι → Type u_6} (t : (i : ι) → Finset (κ i)) (f : ((i : ι) → i ∈ Finset.univ → κ i) → β) : ∑ x ∈ Finset.univ.pi t, f x = ∑ x ∈ Fintype.piFinset t, f fun (a : ι) (x_1 : a ∈ Finset.univ) => x a

Taking a sum over univ.pi t is the same as taking the sum over Fintype.piFinset t. univ.pi t and Fintype.piFinset t are essentially the same Finset, but differ in the type of their element, univ.pi t is a Finset (Π a ∈ univ, t a) and Fintype.piFinset t is a Finset (Π a, t a).

@[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_finset_product {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ × α → β} : ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (c, a)

theorem Finset.sum_finset_product {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ × α → β} : ∑ p ∈ r, f p = ∑ c ∈ s, ∑ a ∈ t c, f (c, a)

theorem Finset.prod_finset_product' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ → α → β} : ∏ p ∈ r, f p.1 p.2 = ∏ c ∈ s, ∏ a ∈ t c, f c a

theorem Finset.sum_finset_product' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) {f : γ → α → β} : ∑ p ∈ r, f p.1 p.2 = ∑ c ∈ s, ∑ a ∈ t c, f c a

theorem Finset.prod_finset_product_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α × γ → β} : ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (a, c)

theorem Finset.sum_finset_product_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α × γ → β} : ∑ p ∈ r, f p = ∑ c ∈ s, ∑ a ∈ t c, f (a, c)

theorem Finset.prod_finset_product_right' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α → γ → β} : ∏ p ∈ r, f p.1 p.2 = ∏ c ∈ s, ∏ a ∈ t c, f a c

theorem Finset.sum_finset_product_right' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2) {f : α → γ → β} : ∑ p ∈ r, f p.1 p.2 = ∑ c ∈ s, ∑ a ∈ t c, f a c

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 ∈ Finset.filter (fun (j : ι) => g j = g i) s, h j) : ∏ a ∈ Finset.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 ∈ Finset.filter (fun (j : ι) => g j = g i) s, h j) : ∑ a ∈ Finset.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_product {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset γ) (t : Finset α) (f : γ × α → β) : ∏ x ∈ s ×ˢ t, f x = ∏ x ∈ s, ∏ y ∈ t, f (x, y)

The product over a product set equals the product of the fiberwise products. For rewriting in the reverse direction, use Finset.prod_product'.

theorem Finset.sum_product {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset γ) (t : Finset α) (f : γ × α → β) : ∑ x ∈ s ×ˢ t, f x = ∑ x ∈ s, ∑ y ∈ t, f (x, y)

The sum over a product set equals the sum of the fiberwise sums. For rewriting in the reverse direction, use Finset.sum_product'

theorem Finset.prod_product' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset γ) (t : Finset α) (f : γ → α → β) : ∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ x ∈ s, ∏ y ∈ t, f x y

The product over a product set equals the product of the fiberwise products. For rewriting in the reverse direction, use Finset.prod_product.

theorem Finset.sum_product' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset γ) (t : Finset α) (f : γ → α → β) : ∑ x ∈ s ×ˢ t, f x.1 x.2 = ∑ x ∈ s, ∑ y ∈ t, f x y

The sum over a product set equals the sum of the fiberwise sums. For rewriting in the reverse direction, use Finset.sum_product

theorem Finset.prod_product_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset γ) (t : Finset α) (f : γ × α → β) : ∏ x ∈ s ×ˢ t, f x = ∏ y ∈ t, ∏ x ∈ s, f (x, y)

theorem Finset.sum_product_right {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset γ) (t : Finset α) (f : γ × α → β) : ∑ x ∈ s ×ˢ t, f x = ∑ y ∈ t, ∑ x ∈ s, f (x, y)

theorem Finset.prod_product_right' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] (s : Finset γ) (t : Finset α) (f : γ → α → β) : ∏ x ∈ s ×ˢ t, f x.1 x.2 = ∏ y ∈ t, ∏ x ∈ s, f x y

An uncurried version of Finset.prod_product_right.

theorem Finset.sum_product_right' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] (s : Finset γ) (t : Finset α) (f : γ → α → β) : ∑ x ∈ s ×ˢ t, f x.1 x.2 = ∑ y ∈ t, ∑ x ∈ s, f x y

An uncurried version of Finset.sum_product_right

theorem Finset.prod_comm' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset γ} {t : γ → Finset α} {t' : Finset α} {s' : α → Finset γ} (h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') {f : γ → α → β} : ∏ x ∈ s, ∏ y ∈ t x, f x y = ∏ y ∈ t', ∏ x ∈ s' y, f x y

Generalization of Finset.prod_comm to the case when the inner Finsets depend on the outer variable.

theorem Finset.sum_comm' {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset γ} {t : γ → Finset α} {t' : Finset α} {s' : α → Finset γ} (h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') {f : γ → α → β} : ∑ x ∈ s, ∑ y ∈ t x, f x y = ∑ y ∈ t', ∑ x ∈ s' y, f x y

Generalization of Finset.sum_comm to the case when the inner Finsets depend on the outer variable.

theorem Finset.prod_comm {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} : ∏ x ∈ s, ∏ y ∈ t, f x y = ∏ y ∈ t, ∏ x ∈ s, f x y

theorem Finset.sum_comm {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} : ∑ x ∈ s, ∑ y ∈ t, f x y = ∑ y ∈ t, ∑ x ∈ s, f x y

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 ∈ Finset.filter (fun (x : α) => p x) s, 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 ∈ Finset.filter (fun (x : α) => p x) s, 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 ∈ Finset.filter (fun (x : α) => f x ≠ 1) s, 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 ∈ Finset.filter (fun (x : α) => f x ≠ 0) s, 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 ∈ Finset.filter (fun (a : α) => p a) s, 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 ∈ Finset.filter (fun (a : α) => p a) s, 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_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 ∈ Finset.filter (fun (x : α) => p x) s, 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 ∈ Finset.filter (fun (x : α) => p x) s, 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 ∈ Finset.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 ∈ Finset.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_preimage' {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [CommMonoid β] (f : ι → κ) [DecidablePred fun (x : κ) => x ∈ Set.range f] (s : Finset κ) (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β) : ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ Finset.filter (fun (x : κ) => x ∈ Set.range f) s, g x

theorem Finset.sum_preimage' {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [AddCommMonoid β] (f : ι → κ) [DecidablePred fun (x : κ) => x ∈ Set.range f] (s : Finset κ) (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β) : ∑ x ∈ s.preimage f hf, g (f x) = ∑ x ∈ Finset.filter (fun (x : κ) => x ∈ Set.range f) s, g x

theorem Finset.prod_preimage {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [CommMonoid β] (f : ι → κ) (s : Finset κ) (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β) (hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1) : ∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x

theorem Finset.sum_preimage {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [AddCommMonoid β] (f : ι → κ) (s : Finset κ) (hf : Set.InjOn f (f ⁻¹' ↑s)) (g : κ → β) (hg : ∀ x ∈ s, x ∉ Set.range f → g x = 0) : ∑ x ∈ s.preimage f hf, g (f x) = ∑ x ∈ s, g x

theorem Finset.prod_preimage_of_bij {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [CommMonoid β] (f : ι → κ) (s : Finset κ) (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) (g : κ → β) : ∏ x ∈ s.preimage f ⋯, g (f x) = ∏ x ∈ s, g x

theorem Finset.sum_preimage_of_bij {ι : Type u_1} {κ : Type u_2} {β : Type u_4} [AddCommMonoid β] (f : ι → κ) (s : Finset κ) (hf : Set.BijOn f (f ⁻¹' ↑s) ↑s) (g : κ → β) : ∑ x ∈ s.preimage f ⋯, g (f x) = ∑ x ∈ s, g x

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) : Finset.univ.prod f = Finset.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) : Finset.univ.sum f = Finset.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_apply_dite {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} [DecidablePred fun (x : α) => ¬p x] (f : (x : α) → p x → γ) (g : (x : α) → ¬p x → γ) (h : γ → β) : ∏ x ∈ s, h (if hx : p x then f x hx else g x hx) = (∏ x : { x : α // x ∈ Finset.filter (fun (x : α) => p x) s }, h (f ↑x ⋯)) * ∏ x : { x : α // x ∈ Finset.filter (fun (x : α) => ¬p x) s }, h (g ↑x ⋯)

theorem Finset.sum_apply_dite {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} [DecidablePred fun (x : α) => ¬p x] (f : (x : α) → p x → γ) (g : (x : α) → ¬p x → γ) (h : γ → β) : ∑ x ∈ s, h (if hx : p x then f x hx else g x hx) = ∑ x : { x : α // x ∈ Finset.filter (fun (x : α) => p x) s }, h (f ↑x ⋯) + ∑ x : { x : α // x ∈ Finset.filter (fun (x : α) => ¬p x) s }, h (g ↑x ⋯)

theorem Finset.prod_apply_ite {α : Type u_3} {β : Type u_4} {γ : Type u_5} [CommMonoid β] {s : Finset α} {p : α → Prop} {_hp : DecidablePred p} (f g : α → γ) (h : γ → β) : ∏ x ∈ s, h (if p x then f x else g x) = (∏ x ∈ Finset.filter (fun (x : α) => p x) s, h (f x)) * ∏ x ∈ Finset.filter (fun (x : α) => ¬p x) s, h (g x)

theorem Finset.sum_apply_ite {α : Type u_3} {β : Type u_4} {γ : Type u_5} [AddCommMonoid β] {s : Finset α} {p : α → Prop} {_hp : DecidablePred p} (f g : α → γ) (h : γ → β) : ∑ x ∈ s, h (if p x then f x else g x) = ∑ x ∈ Finset.filter (fun (x : α) => p x) s, h (f x) + ∑ x ∈ Finset.filter (fun (x : α) => ¬p x) s, h (g x)

theorem Finset.prod_dite {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (∏ x ∈ s, if hx : p x then f x hx else g x hx) = (∏ x : { x : α // x ∈ Finset.filter (fun (x : α) => p x) s }, f ↑x ⋯) * ∏ x : { x : α // x ∈ Finset.filter (fun (x : α) => ¬p x) s }, g ↑x ⋯

theorem Finset.sum_dite {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (∑ x ∈ s, if hx : p x then f x hx else g x hx) = ∑ x : { x : α // x ∈ Finset.filter (fun (x : α) => p x) s }, f ↑x ⋯ + ∑ x : { x : α // x ∈ Finset.filter (fun (x : α) => ¬p x) s }, g ↑x ⋯

theorem Finset.prod_ite {α : Type u_3} {β : Type u_4} [CommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f g : α → β) : (∏ x ∈ s, if p x then f x else g x) = (∏ x ∈ Finset.filter (fun (x : α) => p x) s, f x) * ∏ x ∈ Finset.filter (fun (x : α) => ¬p x) s, g x

theorem Finset.sum_ite {α : Type u_3} {β : Type u_4} [AddCommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f g : α → β) : (∑ x ∈ s, if p x then f x else g x) = ∑ x ∈ Finset.filter (fun (x : α) => p x) s, f x + ∑ x ∈ Finset.filter (fun (x : α) => ¬p x) s, g x

theorem Finset.prod_dite_of_false {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] {p : α → Prop} {x✝ : DecidablePred p} (h : ∀ i ∈ s, ¬p i) (f : (i : α) → p i → β) (g : (i : α) → ¬p i → β) : (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i : { x : α // x ∈ s }, g ↑i ⋯

theorem Finset.sum_dite_of_false {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {x✝ : DecidablePred p} (h : ∀ i ∈ s, ¬p i) (f : (i : α) → p i → β) (g : (i : α) → ¬p i → β) : (∑ i ∈ s, if hi : p i then f i hi else g i hi) = ∑ i : { x : α // x ∈ s }, g ↑i ⋯

theorem Finset.prod_ite_of_false {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] {p : α → Prop} {x✝ : DecidablePred p} (h : ∀ x ∈ s, ¬p x) (f g : α → β) : (∏ x ∈ s, if p x then f x else g x) = ∏ x ∈ s, g x

theorem Finset.sum_ite_of_false {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {x✝ : DecidablePred p} (h : ∀ x ∈ s, ¬p x) (f g : α → β) : (∑ x ∈ s, if p x then f x else g x) = ∑ x ∈ s, g x

theorem Finset.prod_dite_of_true {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] {p : α → Prop} {x✝ : DecidablePred p} (h : ∀ i ∈ s, p i) (f : (i : α) → p i → β) (g : (i : α) → ¬p i → β) : (∏ i ∈ s, if hi : p i then f i hi else g i hi) = ∏ i : { x : α // x ∈ s }, f ↑i ⋯

theorem Finset.sum_dite_of_true {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {x✝ : DecidablePred p} (h : ∀ i ∈ s, p i) (f : (i : α) → p i → β) (g : (i : α) → ¬p i → β) : (∑ i ∈ s, if hi : p i then f i hi else g i hi) = ∑ i : { x : α // x ∈ s }, f ↑i ⋯

theorem Finset.prod_ite_of_true {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] {p : α → Prop} {x✝ : DecidablePred p} (h : ∀ x ∈ s, p x) (f g : α → β) : (∏ x ∈ s, if p x then f x else g x) = ∏ x ∈ s, f x

theorem Finset.sum_ite_of_true {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {x✝ : DecidablePred p} (h : ∀ x ∈ s, p x) (f g : α → β) : (∑ x ∈ s, if p x then f x else g x) = ∑ x ∈ s, f x

theorem Finset.prod_apply_ite_of_false {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f g : α → γ) (k : γ → β) (h : ∀ x ∈ s, ¬p x) : ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (g x)

theorem Finset.sum_apply_ite_of_false {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f g : α → γ) (k : γ → β) (h : ∀ x ∈ s, ¬p x) : ∑ x ∈ s, k (if p x then f x else g x) = ∑ x ∈ s, k (g x)

theorem Finset.prod_apply_ite_of_true {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f g : α → γ) (k : γ → β) (h : ∀ x ∈ s, p x) : ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (f x)

theorem Finset.sum_apply_ite_of_true {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Finset α} [AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f g : α → γ) (k : γ → β) (h : ∀ x ∈ s, p x) : ∑ x ∈ s, k (if p x then f x else g x) = ∑ x ∈ s, k (f x)

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

@[simp]

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

@[simp]

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

@[simp]

theorem Finset.prod_dite_eq {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → a = x → β) : (∏ x ∈ s, if h : a = x then b x h else 1) = if a ∈ s then b a ⋯ else 1

@[simp]

theorem Finset.sum_dite_eq {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → a = x → β) : (∑ x ∈ s, if h : a = x then b x h else 0) = if a ∈ s then b a ⋯ else 0

@[simp]

theorem Finset.prod_dite_eq' {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → x = a → β) : (∏ x ∈ s, if h : x = a then b x h else 1) = if a ∈ s then b a ⋯ else 1

@[simp]

theorem Finset.sum_dite_eq' {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → x = a → β) : (∑ x ∈ s, if h : x = a then b x h else 0) = if a ∈ s then b a ⋯ else 0

@[simp]

theorem Finset.prod_ite_eq {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (∏ x ∈ s, if a = x then b x else 1) = if a ∈ s then b a else 1

@[simp]

theorem Finset.sum_ite_eq {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (∑ x ∈ s, if a = x then b x else 0) = if a ∈ s then b a else 0

@[simp]

theorem Finset.prod_ite_eq' {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (∏ x ∈ s, if x = a then b x else 1) = if a ∈ s then b a else 1

A product taken over a conditional whose condition is an equality test on the index and whose alternative is 1 has value either the term at that index or 1.

The difference with Finset.prod_ite_eq is that the arguments to Eq are swapped.

@[simp]

theorem Finset.sum_ite_eq' {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (∑ x ∈ s, if x = a then b x else 0) = if a ∈ s then b a else 0

A sum taken over a conditional whose condition is an equality test on the index and whose alternative is 0 has value either the term at that index or 0.

The difference with Finset.sum_ite_eq is that the arguments to Eq are swapped.

theorem Finset.prod_ite_eq_of_mem {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) (h : a ∈ s) : (∏ x ∈ s, if a = x then b x else 1) = b a

theorem Finset.sum_ite_eq_of_mem {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) (h : a ∈ s) : (∑ x ∈ s, if a = x then b x else 0) = b a

theorem Finset.prod_ite_eq_of_mem' {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) (h : a ∈ s) : (∏ x ∈ s, if x = a then b x else 1) = b a

The difference with Finset.prod_ite_eq_of_mem is that the arguments to Eq are swapped.

theorem Finset.sum_ite_eq_of_mem' {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s : Finset α) (a : α) (b : α → β) (h : a ∈ s) : (∑ x ∈ s, if x = a then b x else 0) = b a

@[simp]

theorem Finset.prod_pi_mulSingle' {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (a : α) (x : β) (s : Finset α) : ∏ a' ∈ s, Pi.mulSingle a x a' = if a ∈ s then x else 1

@[simp]

theorem Finset.sum_pi_single' {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (a : α) (x : β) (s : Finset α) : ∑ a' ∈ s, Pi.single a x a' = if a ∈ s then x else 0

@[simp]

theorem Finset.prod_pi_mulSingle {α : Type u_3} {β : α → Type u_6} [DecidableEq α] [(a : α) → CommMonoid (β a)] (a : α) (f : (a : α) → β a) (s : Finset α) : ∏ a' ∈ s, Pi.mulSingle a' (f a') a = if a ∈ s then f a else 1

@[simp]

theorem Finset.sum_pi_single {α : Type u_3} {β : α → Type u_6} [DecidableEq α] [(a : α) → AddCommMonoid (β a)] (a : α) (f : (a : α) → β a) (s : Finset α) : ∑ a' ∈ s, Pi.single a' (f a') a = if a ∈ s then f a else 0

theorem Finset.mulSupport_prod {ι : Type u_1} {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset ι) (f : ι → α → β) : (Function.mulSupport fun (x : α) => ∏ i ∈ s, f i x) ⊆ ⋃ i ∈ s, Function.mulSupport (f i)

theorem Finset.support_sum {ι : Type u_1} {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset ι) (f : ι → α → β) : (Function.support fun (x : α) => ∑ i ∈ s, f i x) ⊆ ⋃ i ∈ s, Function.support (f i)

theorem Finset.prod_mulIndicator_subset_of_eq_one {ι : Type u_1} {α : Type u_3} {β : Type u_4} [CommMonoid β] [One α] (f : ι → α) (g : ι → α → β) {s t : Finset ι} (h : s ⊆ t) (hg : ∀ (a : ι), g a 1 = 1) : ∏ i ∈ t, g i ((↑s).mulIndicator f i) = ∏ i ∈ s, g i (f i)

Consider a product of g i (f i) over a finset. Suppose g is a function such as n ↦ (· ^ n), which maps a second argument of 1 to 1. Then if f is replaced by the corresponding multiplicative indicator function, the finset may be replaced by a possibly larger finset without changing the value of the product.

theorem Finset.sum_indicator_subset_of_eq_zero {ι : Type u_1} {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [Zero α] (f : ι → α) (g : ι → α → β) {s t : Finset ι} (h : s ⊆ t) (hg : ∀ (a : ι), g a 0 = 0) : ∑ i ∈ t, g i ((↑s).indicator f i) = ∑ i ∈ s, g i (f i)

Consider a sum of g i (f i) over a finset. Suppose g is a function such as n ↦ (n • ·), which maps a second argument of 0 to 0 (or a weighted sum of f i * h i or f i • h i, where f gives the weights that are multiplied by some other function h). Then if f is replaced by the corresponding indicator function, the finset may be replaced by a possibly larger finset without changing the value of the sum.

theorem Finset.prod_mulIndicator_subset {ι : Type u_1} {β : Type u_4} [CommMonoid β] (f : ι → β) {s t : Finset ι} (h : s ⊆ t) : ∏ i ∈ t, (↑s).mulIndicator f i = ∏ i ∈ s, f i

Taking the product of an indicator function over a possibly larger finset is the same as taking the original function over the original finset.

theorem Finset.sum_indicator_subset {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] (f : ι → β) {s t : Finset ι} (h : s ⊆ t) : ∑ i ∈ t, (↑s).indicator f i = ∑ i ∈ s, f i

Summing an indicator function over a possibly larger Finset is the same as summing the original function over the original finset.

theorem Finset.prod_mulIndicator_eq_prod_filter {ι : Type u_1} {β : Type u_4} [CommMonoid β] {κ : Type u_6} (s : Finset ι) (f : ι → κ → β) (t : ι → Set κ) (g : ι → κ) [DecidablePred fun (i : ι) => g i ∈ t i] : ∏ i ∈ s, (t i).mulIndicator (f i) (g i) = ∏ i ∈ Finset.filter (fun (i : ι) => g i ∈ t i) s, f i (g i)

theorem Finset.sum_indicator_eq_sum_filter {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] {κ : Type u_6} (s : Finset ι) (f : ι → κ → β) (t : ι → Set κ) (g : ι → κ) [DecidablePred fun (i : ι) => g i ∈ t i] : ∑ i ∈ s, (t i).indicator (f i) (g i) = ∑ i ∈ Finset.filter (fun (i : ι) => g i ∈ t i) s, f i (g i)

theorem Finset.prod_mulIndicator_eq_prod_inter {ι : Type u_1} {β : Type u_4} [CommMonoid β] [DecidableEq ι] (s t : Finset ι) (f : ι → β) : ∏ i ∈ s, (↑t).mulIndicator f i = ∏ i ∈ s ∩ t, f i

theorem Finset.sum_indicator_eq_sum_inter {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] [DecidableEq ι] (s t : Finset ι) (f : ι → β) : ∑ i ∈ s, (↑t).indicator f i = ∑ i ∈ s ∩ t, f i

theorem Finset.mulIndicator_prod {ι : Type u_1} {β : Type u_4} [CommMonoid β] {κ : Type u_6} (s : Finset ι) (t : Set κ) (f : ι → κ → β) : t.mulIndicator (∏ i ∈ s, f i) = ∏ i ∈ s, t.mulIndicator (f i)

theorem Finset.indicator_sum {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] {κ : Type u_6} (s : Finset ι) (t : Set κ) (f : ι → κ → β) : t.indicator (∑ i ∈ s, f i) = ∑ i ∈ s, t.indicator (f i)

theorem Finset.mulIndicator_biUnion {ι : Type u_1} {β : Type u_4} [CommMonoid β] {κ : Type u_7} (s : Finset ι) (t : ι → Set κ) {f : κ → β} (hs : (↑s).PairwiseDisjoint t) : (⋃ i ∈ s, t i).mulIndicator f = fun (a : κ) => ∏ i ∈ s, (t i).mulIndicator f a

theorem Finset.indicator_biUnion {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] {κ : Type u_7} (s : Finset ι) (t : ι → Set κ) {f : κ → β} (hs : (↑s).PairwiseDisjoint t) : (⋃ i ∈ s, t i).indicator f = fun (a : κ) => ∑ i ∈ s, (t i).indicator f a

theorem Finset.mulIndicator_biUnion_apply {ι : Type u_1} {β : Type u_4} [CommMonoid β] {κ : Type u_7} (s : Finset ι) (t : ι → Set κ) {f : κ → β} (h : (↑s).PairwiseDisjoint t) (x : κ) : (⋃ i ∈ s, t i).mulIndicator f x = ∏ i ∈ s, (t i).mulIndicator f x

theorem Finset.indicator_biUnion_apply {ι : Type u_1} {β : Type u_4} [AddCommMonoid β] {κ : Type u_7} (s : Finset ι) (t : ι → Set κ) {f : κ → β} (h : (↑s).PairwiseDisjoint t) (x : κ) : (⋃ i ∈ s, t i).indicator f x = ∑ i ∈ s, (t i).indicator f 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 ∈ Finset.range (n + 1), f x = f n * ∏ x ∈ Finset.range n, f x

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

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

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

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

theorem Finset.sum_range_succ' {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) (n : ℕ) : ∑ k ∈ Finset.range (n + 1), f k = ∑ k ∈ Finset.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 ∈ Finset.range n, u k = ∏ k ∈ Finset.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 ∈ Finset.range n, u k = ∑ k ∈ Finset.range N, u k

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

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

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

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

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

theorem Finset.sum_range_one {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) : ∑ k ∈ Finset.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 ∈ Finset.range n, f k = s n

For any product along {0, ..., n - 1} of a commutative-monoid-valued function, we can verify that it's equal to a different function just by checking ratios of adjacent terms.

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

theorem Finset.sum_range_induction {β : Type u_4} [AddCommMonoid β] (f s : ℕ → β) (base : s 0 = 0) (step : ∀ (n : ℕ), s (n + 1) = s n + f n) (n : ℕ) : ∑ k ∈ Finset.range n, f k = s n

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

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

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

A telescoping product along {0, ..., n - 1} of a commutative group valued function reduces to the ratio of the last and first factors.

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

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

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

A telescoping sum along {0, ..., n-1} of an ℕ-valued function reduces to the difference of the last and first terms when the function we are summing is monotone.

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 ∈ Finset.range n, b

theorem Finset.nsmul_eq_sum_const {β : Type u_4} [AddCommMonoid β] (b : β) (n : ℕ) : n • b = ∑ _k ∈ Finset.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_powersetCard {α : Type u_3} {β : Type u_4} [CommMonoid β] (n : ℕ) (s : Finset α) (f : ℕ → β) : ∏ t ∈ Finset.powersetCard n s, f t.card = f n ^ s.card.choose n

A product over Finset.powersetCard which only depends on the size of the sets is constant.

theorem Finset.sum_powersetCard {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (n : ℕ) (s : Finset α) (f : ℕ → β) : ∑ t ∈ Finset.powersetCard n s, f t.card = s.card.choose n • f n

A sum over Finset.powersetCard which only depends on the size of the sets is constant.

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

theorem Finset.sum_flip {β : Type u_4} [AddCommMonoid β] {n : ℕ} (f : ℕ → β) : ∑ r ∈ Finset.range (n + 1), f (n - r) = ∑ k ∈ Finset.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 ∈ Finset.image g s, f b ^ (Finset.filter (fun (a : α) => g a = b) s).card

The product of the composition of functions f and g, is the product over b ∈ s.image g of f b to the power of the cardinality of the fibre of b. 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 ∈ Finset.image g s, (Finset.filter (fun (a : α) => g a = b) s).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_piecewise {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s t : Finset α) (f g : α → β) : ∏ x ∈ s, t.piecewise f g x = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x

theorem Finset.sum_piecewise {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s t : Finset α) (f g : α → β) : ∑ x ∈ s, t.piecewise f g x = ∑ x ∈ s ∩ t, f x + ∑ x ∈ s \ t, g x

theorem Finset.prod_inter_mul_prod_diff {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s t : Finset α) (f : α → β) : (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, f x = ∏ x ∈ s, f x

theorem Finset.sum_inter_add_sum_diff {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] (s t : Finset α) (f : α → β) : ∑ x ∈ s ∩ t, f x + ∑ x ∈ s \ t, f x = ∑ x ∈ s, f x

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

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

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

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

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

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

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

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

theorem Finset.dvd_prod_of_mem {α : Type u_3} {β : Type u_4} [CommMonoid β] (f : α → β) {a : α} {s : Finset α} (ha : a ∈ s) : f a ∣ ∏ i ∈ s, f i

theorem Finset.prod_partition {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] (R : Setoid α) [DecidableRel ⇑R] : ∏ x ∈ s, f x = ∏ xbar ∈ Finset.image (Quotient.mk R) s, ∏ y ∈ Finset.filter (fun (y : α) => ⟦y⟧ = xbar) s, 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 ∈ Finset.image (Quotient.mk R) s, ∑ y ∈ Finset.filter (fun (y : α) => ⟦y⟧ = xbar) s, 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 ∈ Finset.filter (fun (a : α) => R a x) s, 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 ∈ Finset.filter (fun (a : α) => R a x) s, 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.prod_update_of_not_mem {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∉ s) (f : α → β) (b : β) : ∏ x ∈ s, Function.update f i b x = ∏ x ∈ s, f x

theorem Finset.sum_update_of_not_mem {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∉ s) (f : α → β) (b : β) : ∑ x ∈ s, Function.update f i b x = ∑ x ∈ s, f x

theorem Finset.prod_update_of_mem {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) (b : β) : ∏ x ∈ s, Function.update f i b x = b * ∏ x ∈ s \ {i}, f x

theorem Finset.sum_update_of_mem {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) (b : β) : ∑ x ∈ s, Function.update f i b x = b + ∑ x ∈ s \ {i}, f x

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_ite_one {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (p : α → Prop) [DecidablePred p] (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : β) : (∏ i ∈ s, if p i then a else 1) = if ∃ i ∈ s, p i then a else 1

See also Finset.prod_ite_zero.

theorem Finset.sum_ite_zero {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (p : α → Prop) [DecidablePred p] (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : β) : (∑ i ∈ s, if p i then a else 0) = if ∃ i ∈ s, p i then a else 0

See also Finset.sum_boole.

theorem Finset.prod_erase_lt_of_one_lt {α : Type u_3} {γ : Type u_6} [DecidableEq α] [CommMonoid γ] [Preorder γ] [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 γ] [Preorder γ] [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_pow_boole {α : Type u_3} {β : Type u_4} [CommMonoid β] [DecidableEq α] (s : Finset α) (f : α → β) (a : α) : (∏ x ∈ s, f x ^ if a = x then 1 else 0) = if a ∈ s then f a else 1

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

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.isSquare_prod {ι : Type u_1} {α : Type u_3} {s : Finset ι} [CommMonoid α] (f : ι → α) (h : ∀ c ∈ s, IsSquare (f c)) : IsSquare (∏ i ∈ s, f i)

theorem Finset.even_sum {ι : Type u_1} {α : Type u_3} {s : Finset ι} [AddCommMonoid α] (f : ι → α) (h : ∀ c ∈ s, Even (f c)) : Even (∑ i ∈ s, f i)

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, (Finset.filter (fun (i : ι) => g i = j) s).card = (Finset.filter (fun (i : ι) => g i ∈ t) s).card

theorem Finset.card_filter {ι : Type u_1} (p : ι → Prop) [DecidablePred p] (s : Finset ι) : (Finset.filter (fun (i : ι) => p i) s).card = ∑ i ∈ s, if p i then 1 else 0

@[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_sigma {α : Type u_3} {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a)) : (s.sigma t).card = ∑ a ∈ s, (t a).card

@[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} [DecidableEq β] {s : Finset α} {t : α → Finset β} (h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → Disjoint (t x) (t y)) : (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 : ∀ x ∈ s, f x ∈ t) : s.card = ∑ b ∈ t, (Finset.filter (fun (a : α) => f a = b) s).card

theorem Finset.card_eq_sum_card_image {α : Type u_3} {β : Type u_4} [DecidableEq β] (f : α → β) (s : Finset α) : s.card = ∑ b ∈ Finset.image f s, (Finset.filter (fun (a : α) => f a = b) s).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 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 Fintype.prod_ite_eq_ite_exists {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] (p : ι → Prop) [DecidablePred p] (h : ∀ (i j : ι), p i → p j → i = j) (a : α) : (∏ i : ι, if p i then a else 1) = if ∃ (i : ι), p i then a else 1

theorem Fintype.sum_ite_eq_ite_exists {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] (p : ι → Prop) [DecidablePred p] (h : ∀ (i j : ι), p i → p j → i = j) (a : α) : (∑ i : ι, if p i then a else 0) = if ∃ (i : ι), p i then a else 0

theorem Fintype.prod_ite_mem {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] [DecidableEq ι] (s : Finset ι) (f : ι → α) : (∏ i : ι, if i ∈ s then f i else 1) = ∏ i ∈ s, f i

theorem Fintype.sum_ite_mem {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] [DecidableEq ι] (s : Finset ι) (f : ι → α) : (∑ i : ι, if i ∈ s then f i else 0) = ∑ i ∈ s, f i

theorem Fintype.prod_dite_eq {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] [DecidableEq ι] (i : ι) (f : (j : ι) → i = j → α) : (∏ j : ι, if h : i = j then f j h else 1) = f i ⋯

See also Finset.prod_dite_eq.

theorem Fintype.sum_dite_eq {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] [DecidableEq ι] (i : ι) (f : (j : ι) → i = j → α) : (∑ j : ι, if h : i = j then f j h else 0) = f i ⋯

See also Finset.sum_dite_eq.

theorem Fintype.prod_dite_eq' {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] [DecidableEq ι] (i : ι) (f : (j : ι) → j = i → α) : (∏ j : ι, if h : j = i then f j h else 1) = f i ⋯

See also Finset.prod_dite_eq'.

theorem Fintype.sum_dite_eq' {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] [DecidableEq ι] (i : ι) (f : (j : ι) → j = i → α) : (∑ j : ι, if h : j = i then f j h else 0) = f i ⋯

See also Finset.sum_dite_eq'.

theorem Fintype.prod_ite_eq {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] [DecidableEq ι] (i : ι) (f : ι → α) : (∏ j : ι, if i = j then f j else 1) = f i

See also Finset.prod_ite_eq.

theorem Fintype.sum_ite_eq {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] [DecidableEq ι] (i : ι) (f : ι → α) : (∑ j : ι, if i = j then f j else 0) = f i

See also Finset.sum_ite_eq.

theorem Fintype.prod_ite_eq' {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] [DecidableEq ι] (i : ι) (f : ι → α) : (∏ j : ι, if j = i then f j else 1) = f i

See also Finset.prod_ite_eq'.

theorem Fintype.sum_ite_eq' {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] [DecidableEq ι] (i : ι) (f : ι → α) : (∑ j : ι, if j = i then f j else 0) = f i

See also Finset.sum_ite_eq'.

theorem Fintype.prod_pi_mulSingle {ι : Type u_6} [Fintype ι] [DecidableEq ι] {α : ι → Type u_9} [(i : ι) → CommMonoid (α i)] (i : ι) (f : (i : ι) → α i) : ∏ j : ι, Pi.mulSingle j (f j) i = f i

See also Finset.prod_pi_mulSingle.

theorem Fintype.sum_pi_single {ι : Type u_6} [Fintype ι] [DecidableEq ι] {α : ι → Type u_9} [(i : ι) → AddCommMonoid (α i)] (i : ι) (f : (i : ι) → α i) : ∑ j : ι, Pi.single j (f j) i = f i

See also Finset.sum_pi_single.

theorem Fintype.prod_pi_mulSingle' {ι : Type u_6} {α : Type u_8} [Fintype ι] [CommMonoid α] [DecidableEq ι] (i : ι) (a : α) : ∏ j : ι, Pi.mulSingle i a j = a

See also Finset.prod_pi_mulSingle'.

theorem Fintype.sum_pi_single' {ι : Type u_6} {α : Type u_8} [Fintype ι] [AddCommMonoid α] [DecidableEq ι] (i : ι) (a : α) : ∑ j : ι, Pi.single i a j = a

See also Finset.sum_pi_single'.

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 = (List.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 = (List.map f l).sum

@[simp]

theorem List.sum_toFinset_count_eq_length {α : Type u_3} [DecidableEq α] (l : List α) : ∑ a ∈ l.toFinset, List.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, Multiset.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, Multiset.count a m = m.card

@[deprecated Multiset.sum_count_eq_card (since := "2024-07-21")]

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

@[simp]

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

theorem Multiset.exists_smul_of_dvd_count {α : Type u_3} [DecidableEq α] (s : Multiset α) {k : ℕ} (h : ∀ a ∈ s, k ∣ Multiset.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