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

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)

source

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)

source

@[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 : α → β → γ

source

@[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 : α → β → γ

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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.

source

@[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.

source

@[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.

source

@[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.

source

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

source

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

source

@[simp]

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

∏ x ∈ {a}, f x = f a

source

@[simp]

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

∑ x ∈ {a}, f x = f a

source

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

source

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

source

@[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)

source

@[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)

source

theorem Finset.prod_attach {α : Type u_3} {β : Type u_4} [CommMonoid β] (s : Finset α) (f : α → β) :

∏ x ∈ s.attach, f ↑x = ∏ x ∈ s, f x

source

theorem Finset.sum_attach {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) :

∑ x ∈ s.attach, f ↑x = ∑ x ∈ s, f x

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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 ∈ filter (fun (x : α) => p x) s, f x) * ∏ x ∈ filter (fun (x : α) => ¬p x) s, f x = ∏ x ∈ s, f x

source

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 ∈ filter (fun (x : α) => p x) s, f x + ∑ x ∈ filter (fun (x : α) => ¬p x) s, f x = ∑ x ∈ s, f x

source

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 ∈ filter (fun (x : α) => ¬p x) s, f x) * ∏ x ∈ filter p s, f x = ∏ x ∈ s, f x

source

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 ∈ filter (fun (x : α) => ¬p x) s, f x + ∑ x ∈ filter p s, f x = ∑ x ∈ s, f x

source

theorem Finset.prod_filter_xor {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [CommMonoid β] (p q : α → Prop) [DecidablePred p] [DecidablePred q] :

∏ x ∈ filter (fun (x : α) => Xor' (p x) (q x)) s, f x = (∏ x ∈ filter (fun (x : α) => p x ∧ ¬q x) s, f x) * ∏ x ∈ filter (fun (x : α) => q x ∧ ¬p x) s, f x

source

theorem Finset.sum_filter_xor {α : Type u_3} {β : Type u_4} {s : Finset α} {f : α → β} [AddCommMonoid β] (p q : α → Prop) [DecidablePred p] [DecidablePred q] :

∑ x ∈ filter (fun (x : α) => Xor' (p x) (q x)) s, f x = ∑ x ∈ filter (fun (x : α) => p x ∧ ¬q x) s, f x + ∑ x ∈ filter (fun (x : α) => q x ∧ ¬p x) s, f x

source

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

source

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

source

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.

source

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.

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[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)

source

@[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)

source

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)

source

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)

source

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

source

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

source

@[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.

source

@[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.

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

theorem Finset.prod_fiberwise {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : ι → α) :

∏ j : κ, ∏ i ∈ filter (fun (i : ι) => g i = j) s, f i = ∏ i ∈ s, f i

source

theorem Finset.sum_fiberwise {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : ι → α) :

∑ j : κ, ∑ i ∈ filter (fun (i : ι) => g i = j) s, f i = ∑ i ∈ s, f i

source

theorem Finset.prod_fiberwise' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [CommMonoid α] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : κ → α) :

∏ j : κ, ∏ i ∈ filter (fun (i : ι) => g i = j) s, f j = ∏ i ∈ s, f (g i)

source

theorem Finset.sum_fiberwise' {ι : Type u_6} {κ : Type u_7} {α : Type u_8} [AddCommMonoid α] [DecidableEq κ] [Fintype κ] (s : Finset ι) (g : ι → κ) (f : κ → α) :

∑ j : κ, ∑ i ∈ filter (fun (i : ι) => g i = j) s, f j = ∑ i ∈ s, f (g i)

source

@[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)

source

@[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)

source

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

∏ a ∈ image g s, f a = ∏ i ∈ s, h i

source

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

∑ a ∈ image g s, f a = ∑ i ∈ s, h i

source

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

source

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

source

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

source

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)

source

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 ∈ filter (fun (x : α) => p x) s, f x = ∏ x ∈ s, f x

source

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 ∈ filter (fun (x : α) => p x) s, f x = ∑ x ∈ s, f x

source

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

∏ x ∈ filter (fun (x : α) => f x ≠ 1) s, f x = ∏ x ∈ s, f x

source

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

∑ x ∈ filter (fun (x : α) => f x ≠ 0) s, f x = ∑ x ∈ s, f x

source

theorem Finset.prod_filter {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] (p : α → Prop) [DecidablePred p] (f : α → β) :

∏ a ∈ filter (fun (a : α) => p a) s, f a = ∏ a ∈ s, if p a then f a else 1

source

theorem Finset.sum_filter {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] (p : α → Prop) [DecidablePred p] (f : α → β) :

∑ a ∈ filter (fun (a : α) => p a) s, f a = ∑ a ∈ s, if p a then f a else 0

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

@[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 ∈ filter (fun (x : α) => p x) s, f x

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

source

@[simp]

theorem Finset.sum_subtype_eq_sum_filter {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] (f : α → β) {p : α → Prop} [DecidablePred p] :

∑ x ∈ Finset.subtype p s, f ↑x = ∑ x ∈ filter (fun (x : α) => p x) s, f x

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

source

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.

source

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.

source

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.

source

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.

source

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

source

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

source

theorem Finset.prod_finset_coe {α : Type u_3} {β : Type u_4} [CommMonoid β] (f : α → β) (s : Finset α) :

∏ i : ↑↑s, f ↑i = ∏ i ∈ s, f i

source

theorem Finset.sum_finset_coe {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (f : α → β) (s : Finset α) :

∑ i : ↑↑s, f ↑i = ∑ i ∈ s, f i

source

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

source

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

source

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

source

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

source

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.

source

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.

source

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 ∈ filter (fun (x : α) => p x) s }, h (f ↑x ⋯)) * ∏ x : { x : α // x ∈ filter (fun (x : α) => ¬p x) s }, h (g ↑x ⋯)

source

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 ∈ filter (fun (x : α) => p x) s }, h (f ↑x ⋯) + ∑ x : { x : α // x ∈ filter (fun (x : α) => ¬p x) s }, h (g ↑x ⋯)

source

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 ∈ filter (fun (x : α) => p x) s, h (f x)) * ∏ x ∈ filter (fun (x : α) => ¬p x) s, h (g x)

source

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 ∈ filter (fun (x : α) => p x) s, h (f x) + ∑ x ∈ filter (fun (x : α) => ¬p x) s, h (g x)

source

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 ∈ filter (fun (x : α) => p x) s }, f ↑x ⋯) * ∏ x : { x : α // x ∈ filter (fun (x : α) => ¬p x) s }, g ↑x ⋯

source

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 ∈ filter (fun (x : α) => p x) s }, f ↑x ⋯ + ∑ x : { x : α // x ∈ filter (fun (x : α) => ¬p x) s }, g ↑x ⋯

source

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 ∈ filter (fun (x : α) => p x) s, f x) * ∏ x ∈ filter (fun (x : α) => ¬p x) s, g x

source

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 ∈ filter (fun (x : α) => p x) s, f x + ∑ x ∈ filter (fun (x : α) => ¬p x) s, g x

source

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 ⋯

source

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 ⋯

source

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

source

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

source

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 ⋯

source

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 ⋯

source

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

source

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

source

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)

source

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)

source

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)

source

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)

source

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

source

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

source

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

source

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

source

@[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

source

@[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

source

theorem Finset.prod_attach_eq_prod_dite {α : Type u_3} {β : Type u_4} [CommMonoid β] [Fintype α] (s : Finset α) (f : { x : α // x ∈ s } → β) [DecidablePred fun (x : α) => x ∈ s] :

∏ i ∈ s.attach, f i = ∏ i : α, if h : i ∈ s then f ⟨i, h⟩ else 1

source

theorem Finset.sum_attach_eq_sum_dite {α : Type u_3} {β : Type u_4} [AddCommMonoid β] [Fintype α] (s : Finset α) (f : { x : α // x ∈ s } → β) [DecidablePred fun (x : α) => x ∈ s] :

∑ i ∈ s.attach, f i = ∑ i : α, if h : i ∈ s then f ⟨i, h⟩ else 0

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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.

source

@[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.

source

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

source

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

source

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.

source

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

source

@[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

source

@[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

source

@[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

source

@[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

source

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)

source

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)

source

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.

source

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.

source

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.

source

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.

source

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

source

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

source

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

source

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

source

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)

source

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)

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

theorem Finset.prod_range_succ {β : Type u_4} [CommMonoid β] (f : ℕ → β) (n : ℕ) :

∏ x ∈ range (n + 1), f x = (∏ x ∈ range n, f x) * f n

source

theorem Finset.sum_range_succ {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) (n : ℕ) :

∑ x ∈ range (n + 1), f x = ∑ x ∈ range n, f x + f n

source

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

source

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

source

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

source

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

source

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)

source

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)

source

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)

source

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)

source

theorem Finset.prod_range_one {β : Type u_4} [CommMonoid β] (f : ℕ → β) :

∏ k ∈ range 1, f k = f 0

source

theorem Finset.sum_range_one {β : Type u_4} [AddCommMonoid β] (f : ℕ → β) :

∑ k ∈ range 1, f k = f 0

source

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

source

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

source

theorem Finset.prod_list_count {α : Type u_3} [DecidableEq α] [CommMonoid α] (s : List α) :

s.prod = ∏ m ∈ s.toFinset, m ^ List.count m s

source

theorem Finset.sum_list_count {α : Type u_3} [DecidableEq α] [AddCommMonoid α] (s : List α) :

s.sum = ∑ m ∈ s.toFinset, List.count m s • m

source

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

source

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

source

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

source

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

source

theorem Finset.prod_multiset_count {α : Type u_3} [DecidableEq α] [CommMonoid α] (s : Multiset α) :

s.prod = ∏ m ∈ s.toFinset, m ^ Multiset.count m s

source

theorem Finset.sum_multiset_count {α : Type u_3} [DecidableEq α] [AddCommMonoid α] (s : Multiset α) :

s.sum = ∑ m ∈ s.toFinset, Multiset.count m s • m

source

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

source

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

source

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.

source

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.

source

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.

source

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.

source

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

source

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

source

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

source

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)

source

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)

source

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)

source

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.

source

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

source

@[simp]

theorem Finset.prod_const {α : Type u_3} {β : Type u_4} {s : Finset α} [CommMonoid β] (b : β) :

∏ _x ∈ s, b = b ^ s.card

source

@[simp]

theorem Finset.sum_const {α : Type u_3} {β : Type u_4} {s : Finset α} [AddCommMonoid β] (b : β) :

∑ _x ∈ s, b = s.card • b

source

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

source

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

source

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

source

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)

source

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

source

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)

source

theorem Finset.pow_eq_prod_const {β : Type u_4} [CommMonoid β] (b : β) (n : ℕ) :

b ^ n = ∏ _k ∈ range n, b

source

theorem Finset.nsmul_eq_sum_const {β : Type u_4} [AddCommMonoid β] (b : β) (n : ℕ) :

n • b = ∑ _k ∈ range n, b

source

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

source

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

source

theorem Finset.prod_flip {β : Type u_4} [CommMonoid β] {n : ℕ} (f : ℕ → β) :

∏ r ∈ range (n + 1), f (n - r) = ∏ k ∈ range (n + 1), f k

source

theorem Finset.sum_flip {β : Type u_4} [AddCommMonoid β] {n : ℕ} (f : ℕ → β) :

∑ r ∈ range (n + 1), f (n - r) = ∑ k ∈ range (n + 1), f k

source

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.

source

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.

source

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.

source

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.

source

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 ^ (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.

source

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, (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.

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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 ∈ filter (fun (y : α) => ⟦y⟧ = xbar) s, f y

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

source

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 ∈ filter (fun (y : α) => ⟦y⟧ = xbar) s, f y

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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.

source

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

Documentation

Mathlib.Algebra.BigOperators.Group.Finset.Basic

Big operators #