Big operators

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

Notation

We introduce the following notation, localized in BigOperators. To enable the notation, use open BigOperators.

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

• ∏ x in s, f x is notation for Finset.prod s f (assuming β is a CommMonoid)
• ∑ x in 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.

ink

def Finset.sum {β : Type u} {α : Type v} [inst : AddCommMonoid β] (s : Finset α) (f : α → β) : β

∑ x in s, f x is the sum of f x as x ranges over the elements of the finite set s.

Equations

• Finset.sum s f = Multiset.sum (Multiset.map f s.val)

ink

def Finset.prod {β : Type u} {α : Type v} [inst : CommMonoid β] (s : Finset α) (f : α → β) : β

∏ x in s, f x is the product of f x as x ranges over the elements of the finite set s.

Equations

• Finset.prod s f = Multiset.prod (Multiset.map f s.val)

ink

@[simp]

theorem Finset.sum_mk {β : Type u} {α : Type v} [inst : AddCommMonoid β] (s : Multiset α) (hs : Multiset.Nodup s) (f : α → β) : Finset.sum { val := s, nodup := hs } f = Multiset.sum (Multiset.map f s)

ink

@[simp]

theorem Finset.prod_mk {β : Type u} {α : Type v} [inst : CommMonoid β] (s : Multiset α) (hs : Multiset.Nodup s) (f : α → β) : Finset.prod { val := s, nodup := hs } f = Multiset.prod (Multiset.map f s)

ink

@[simp]

theorem Finset.sum_val {α : Type v} [inst : AddCommMonoid α] (s : Finset α) : Multiset.sum s.val = Finset.sum s id

ink

@[simp]

theorem Finset.prod_val {α : Type v} [inst : CommMonoid α] (s : Finset α) : Multiset.prod s.val = Finset.prod s id

ink

def BigOperators.bigsum : Lean.ParserDescr

∑ x, f x is notation for Finset.sum Finset.univ f. It is the sum of f x, where x ranges over the finite domain of f.

Equations

• One or more equations did not get rendered due to their size.

ink

def BigOperators.bigprod : Lean.ParserDescr

∏ x, f x is notation for Finset.prod Finset.univ f. It is the product of f x, where x ranges over the finite domain of f.

Equations

• One or more equations did not get rendered due to their size.

ink

def BigOperators.bigsumin : Lean.ParserDescr

∑ x in s, f x is notation for Finset.sum s f. It is the sum of f x, where x ranges over the finite set s.

Equations

• One or more equations did not get rendered due to their size.

ink

def BigOperators.bigprodin : Lean.ParserDescr

∏ x, f x is notation for Finset.prod s f. It is the sum of f x, where x ranges over the finite set s.

Equations

• One or more equations did not get rendered due to their size.

ink

theorem Finset.sum_eq_multiset_sum {β : Type u} {α : Type v} [inst : AddCommMonoid β] (s : Finset α) (f : α → β) : (Finset.sum s fun x => f x) = Multiset.sum (Multiset.map f s.val)

ink

theorem Finset.prod_eq_multiset_prod {β : Type u} {α : Type v} [inst : CommMonoid β] (s : Finset α) (f : α → β) : (Finset.prod s fun x => f x) = Multiset.prod (Multiset.map f s.val)

ink

theorem Finset.sum_eq_fold {β : Type u} {α : Type v} [inst : AddCommMonoid β] (s : Finset α) (f : α → β) : (Finset.sum s fun x => f x) = Finset.fold (fun x x_1 => x + x_1) 0 f s

ink

theorem Finset.prod_eq_fold {β : Type u} {α : Type v} [inst : CommMonoid β] (s : Finset α) (f : α → β) : (Finset.prod s fun x => f x) = Finset.fold (fun x x_1 => x * x_1) 1 f s

ink

@[simp]

theorem Finset.sum_multiset_singleton {α : Type v} (s : Finset α) : (Finset.sum s fun x => {x}) = s.val

ink

theorem map_sum {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] [inst : AddCommMonoid γ] {G : Type u_1} [inst : AddMonoidHomClass G β γ] (g : G) (f : α → β) (s : Finset α) : ↑g (Finset.sum s fun x => f x) = Finset.sum s fun x => ↑g (f x)

ink

theorem map_prod {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] [inst : CommMonoid γ] {G : Type u_1} [inst : MonoidHomClass G β γ] (g : G) (f : α → β) (s : Finset α) : ↑g (Finset.prod s fun x => f x) = Finset.prod s fun x => ↑g (f x)

ink

theorem AddMonoidHom.map_sum {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] [inst : AddCommMonoid γ] (g : β →+ γ) (f : α → β) (s : Finset α) : ↑g (Finset.sum s fun x => f x) = Finset.sum s fun x => ↑g (f x)

Deprecated: use _root_.map_sum instead.

ink

theorem MonoidHom.map_prod {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] [inst : CommMonoid γ] (g : β →* γ) (f : α → β) (s : Finset α) : ↑g (Finset.prod s fun x => f x) = Finset.prod s fun x => ↑g (f x)

Deprecated: use _root_.map_prod instead.

ink

theorem AddEquiv.map_sum {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] [inst : AddCommMonoid γ] (g : β ≃+ γ) (f : α → β) (s : Finset α) : ↑g (Finset.sum s fun x => f x) = Finset.sum s fun x => ↑g (f x)

Deprecated: use _root_.map_sum instead.

ink

theorem MulEquiv.map_prod {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] [inst : CommMonoid γ] (g : β ≃* γ) (f : α → β) (s : Finset α) : ↑g (Finset.prod s fun x => f x) = Finset.prod s fun x => ↑g (f x)

Deprecated: use _root_.map_prod instead.

ink

theorem RingHom.map_list_prod {β : Type u} {γ : Type w} [inst : Semiring β] [inst : Semiring γ] (f : β →+* γ) (l : List β) : ↑f (List.prod l) = List.prod (List.map (↑f) l)

ink

theorem RingHom.map_list_sum {β : Type u} {γ : Type w} [inst : NonAssocSemiring β] [inst : NonAssocSemiring γ] (f : β →+* γ) (l : List β) : ↑f (List.sum l) = List.sum (List.map (↑f) l)

ink

theorem RingHom.unop_map_list_prod {β : Type u} {γ : Type w} [inst : Semiring β] [inst : Semiring γ] (f : β →+* γᵐᵒᵖ) (l : List β) : (↑f (List.prod l)).unop = List.prod (List.reverse (List.map (MulOpposite.unop ∘ ↑f) l))

A morphism into the opposite ring acts on the product by acting on the reversed elements.

ink

theorem RingHom.map_multiset_prod {β : Type u} {γ : Type w} [inst : CommSemiring β] [inst : CommSemiring γ] (f : β →+* γ) (s : Multiset β) : ↑f (Multiset.prod s) = Multiset.prod (Multiset.map (↑f) s)

ink

theorem RingHom.map_multiset_sum {β : Type u} {γ : Type w} [inst : NonAssocSemiring β] [inst : NonAssocSemiring γ] (f : β →+* γ) (s : Multiset β) : ↑f (Multiset.sum s) = Multiset.sum (Multiset.map (↑f) s)

ink

theorem RingHom.map_prod {β : Type u} {α : Type v} {γ : Type w} [inst : CommSemiring β] [inst : CommSemiring γ] (g : β →+* γ) (f : α → β) (s : Finset α) : ↑g (Finset.prod s fun x => f x) = Finset.prod s fun x => ↑g (f x)

ink

theorem RingHom.map_sum {β : Type u} {α : Type v} {γ : Type w} [inst : NonAssocSemiring β] [inst : NonAssocSemiring γ] (g : β →+* γ) (f : α → β) (s : Finset α) : ↑g (Finset.sum s fun x => f x) = Finset.sum s fun x => ↑g (f x)

ink

theorem AddMonoidHom.coe_finset_sum {β : Type u} {α : Type v} {γ : Type w} [inst : AddZeroClass β] [inst : AddCommMonoid γ] (f : α → β →+ γ) (s : Finset α) : ↑(Finset.sum s fun x => f x) = Finset.sum s fun x => ↑(f x)

ink

theorem MonoidHom.coe_finset_prod {β : Type u} {α : Type v} {γ : Type w} [inst : MulOneClass β] [inst : CommMonoid γ] (f : α → β →* γ) (s : Finset α) : ↑(Finset.prod s fun x => f x) = Finset.prod s fun x => ↑(f x)

ink

@[simp]

theorem AddMonoidHom.finset_sum_apply {β : Type u} {α : Type v} {γ : Type w} [inst : AddZeroClass β] [inst : AddCommMonoid γ] (f : α → β →+ γ) (s : Finset α) (b : β) : ↑(Finset.sum s fun x => f x) b = Finset.sum s fun x => ↑(f x) b

ink

@[simp]

theorem MonoidHom.finset_prod_apply {β : Type u} {α : Type v} {γ : Type w} [inst : MulOneClass β] [inst : CommMonoid γ] (f : α → β →* γ) (s : Finset α) (b : β) : ↑(Finset.prod s fun x => f x) b = Finset.prod s fun x => ↑(f x) b

ink

@[simp]

theorem Finset.sum_empty {β : Type u} {α : Type v} {f : α → β} [inst : AddCommMonoid β] : (Finset.sum ∅ fun x => f x) = 0

ink

@[simp]

theorem Finset.prod_empty {β : Type u} {α : Type v} {f : α → β} [inst : CommMonoid β] : (Finset.prod ∅ fun x => f x) = 1

ink

theorem Finset.sum_of_empty {β : Type u} {α : Type v} {f : α → β} [inst : AddCommMonoid β] [inst : IsEmpty α] (s : Finset α) : (Finset.sum s fun i => f i) = 0

ink

theorem Finset.prod_of_empty {β : Type u} {α : Type v} {f : α → β} [inst : CommMonoid β] [inst : IsEmpty α] (s : Finset α) : (Finset.prod s fun i => f i) = 1

ink

@[simp]

theorem Finset.sum_cons {β : Type u} {α : Type v} {s : Finset α} {a : α} {f : α → β} [inst : AddCommMonoid β] (h : ¬a ∈ s) : (Finset.sum (Finset.cons a s h) fun x => f x) = f a + Finset.sum s fun x => f x

ink

@[simp]

theorem Finset.prod_cons {β : Type u} {α : Type v} {s : Finset α} {a : α} {f : α → β} [inst : CommMonoid β] (h : ¬a ∈ s) : (Finset.prod (Finset.cons a s h) fun x => f x) = f a * Finset.prod s fun x => f x

ink

@[simp]

theorem Finset.sum_insert {β : Type u} {α : Type v} {s : Finset α} {a : α} {f : α → β} [inst : AddCommMonoid β] [inst : DecidableEq α] : ¬a ∈ s → (Finset.sum (insert a s) fun x => f x) = f a + Finset.sum s fun x => f x

ink

@[simp]

theorem Finset.prod_insert {β : Type u} {α : Type v} {s : Finset α} {a : α} {f : α → β} [inst : CommMonoid β] [inst : DecidableEq α] : ¬a ∈ s → (Finset.prod (insert a s) fun x => f x) = f a * Finset.prod s fun x => f x

ink

@[simp]

theorem Finset.sum_insert_of_eq_zero_if_not_mem {β : Type u} {α : Type v} {s : Finset α} {a : α} {f : α → β} [inst : AddCommMonoid β] [inst : DecidableEq α] (h : ¬a ∈ s → f a = 0) : (Finset.sum (insert a s) fun x => f x) = Finset.sum s fun x => 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.

ink

@[simp]

theorem Finset.prod_insert_of_eq_one_if_not_mem {β : Type u} {α : Type v} {s : Finset α} {a : α} {f : α → β} [inst : CommMonoid β] [inst : DecidableEq α] (h : ¬a ∈ s → f a = 1) : (Finset.prod (insert a s) fun x => f x) = Finset.prod s fun x => 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.

ink

@[simp]

theorem Finset.sum_insert_zero {β : Type u} {α : Type v} {s : Finset α} {a : α} {f : α → β} [inst : AddCommMonoid β] [inst : DecidableEq α] (h : f a = 0) : (Finset.sum (insert a s) fun x => f x) = Finset.sum s fun x => f x

The sum of f over insert a s is the same as the sum over s, as long as f a = 0.

ink

@[simp]

theorem Finset.prod_insert_one {β : Type u} {α : Type v} {s : Finset α} {a : α} {f : α → β} [inst : CommMonoid β] [inst : DecidableEq α] (h : f a = 1) : (Finset.prod (insert a s) fun x => f x) = Finset.prod s fun x => f x

The product of f over insert a s is the same as the product over s, as long as f a = 1.

ink

@[simp]

theorem Finset.sum_singleton {β : Type u} {α : Type v} {a : α} {f : α → β} [inst : AddCommMonoid β] : (Finset.sum {a} fun x => f x) = f a

ink

@[simp]

theorem Finset.prod_singleton {β : Type u} {α : Type v} {a : α} {f : α → β} [inst : CommMonoid β] : (Finset.prod {a} fun x => f x) = f a

ink

theorem Finset.sum_pair {β : Type u} {α : Type v} {f : α → β} [inst : AddCommMonoid β] [inst : DecidableEq α] {a : α} {b : α} (h : a ≠ b) : (Finset.sum {a, b} fun x => f x) = f a + f b

ink

theorem Finset.prod_pair {β : Type u} {α : Type v} {f : α → β} [inst : CommMonoid β] [inst : DecidableEq α] {a : α} {b : α} (h : a ≠ b) : (Finset.prod {a, b} fun x => f x) = f a * f b

ink

@[simp]

theorem Finset.sum_const_zero {β : Type u} {α : Type v} {s : Finset α} [inst : AddCommMonoid β] : (Finset.sum s fun _x => 0) = 0

ink

@[simp]

theorem Finset.prod_const_one {β : Type u} {α : Type v} {s : Finset α} [inst : CommMonoid β] : (Finset.prod s fun _x => 1) = 1

ink

@[simp]

theorem Finset.sum_image {β : Type u} {α : Type v} {γ : Type w} {f : α → β} [inst : AddCommMonoid β] [inst : DecidableEq α] {s : Finset γ} {g : γ → α} : (∀ (x : γ), x ∈ s → ∀ (y : γ), y ∈ s → g x = g y → x = y) → (Finset.sum (Finset.image g s) fun x => f x) = Finset.sum s fun x => f (g x)

ink

@[simp]

theorem Finset.prod_image {β : Type u} {α : Type v} {γ : Type w} {f : α → β} [inst : CommMonoid β] [inst : DecidableEq α] {s : Finset γ} {g : γ → α} : (∀ (x : γ), x ∈ s → ∀ (y : γ), y ∈ s → g x = g y → x = y) → (Finset.prod (Finset.image g s) fun x => f x) = Finset.prod s fun x => f (g x)

ink

@[simp]

theorem Finset.sum_map {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] (s : Finset α) (e : α ↪ γ) (f : γ → β) : (Finset.sum (Finset.map e s) fun x => f x) = Finset.sum s fun x => f (↑e x)

ink

@[simp]

theorem Finset.prod_map {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] (s : Finset α) (e : α ↪ γ) (f : γ → β) : (Finset.prod (Finset.map e s) fun x => f x) = Finset.prod s fun x => f (↑e x)

ink

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

ink

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

ink

theorem Finset.sum_disjUnion {β : Type u} {α : Type v} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [inst : AddCommMonoid β] (h : Disjoint s₁ s₂) : (Finset.sum (Finset.disjUnion s₁ s₂ h) fun x => f x) = (Finset.sum s₁ fun x => f x) + Finset.sum s₂ fun x => f x

ink

theorem Finset.prod_disjUnion {β : Type u} {α : Type v} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [inst : CommMonoid β] (h : Disjoint s₁ s₂) : (Finset.prod (Finset.disjUnion s₁ s₂ h) fun x => f x) = (Finset.prod s₁ fun x => f x) * Finset.prod s₂ fun x => f x

ink

theorem Finset.sum_disjUnionᵢ {ι : Type u_1} {β : Type u} {α : Type v} {f : α → β} [inst : AddCommMonoid β] (s : Finset ι) (t : ι → Finset α) (h : Set.PairwiseDisjoint (↑s) t) : (Finset.sum (Finset.disjUnionᵢ s t h) fun x => f x) = Finset.sum s fun i => Finset.sum (t i) fun x => f x

ink

theorem Finset.prod_disjUnionᵢ {ι : Type u_1} {β : Type u} {α : Type v} {f : α → β} [inst : CommMonoid β] (s : Finset ι) (t : ι → Finset α) (h : Set.PairwiseDisjoint (↑s) t) : (Finset.prod (Finset.disjUnionᵢ s t h) fun x => f x) = Finset.prod s fun i => Finset.prod (t i) fun x => f x

ink

theorem Finset.sum_union_inter {β : Type u} {α : Type v} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [inst : AddCommMonoid β] [inst : DecidableEq α] : ((Finset.sum (s₁ ∪ s₂) fun x => f x) + Finset.sum (s₁ ∩ s₂) fun x => f x) = (Finset.sum s₁ fun x => f x) + Finset.sum s₂ fun x => f x

ink

theorem Finset.prod_union_inter {β : Type u} {α : Type v} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [inst : CommMonoid β] [inst : DecidableEq α] : ((Finset.prod (s₁ ∪ s₂) fun x => f x) * Finset.prod (s₁ ∩ s₂) fun x => f x) = (Finset.prod s₁ fun x => f x) * Finset.prod s₂ fun x => f x

ink

theorem Finset.sum_union {β : Type u} {α : Type v} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [inst : AddCommMonoid β] [inst : DecidableEq α] (h : Disjoint s₁ s₂) : (Finset.sum (s₁ ∪ s₂) fun x => f x) = (Finset.sum s₁ fun x => f x) + Finset.sum s₂ fun x => f x

ink

theorem Finset.prod_union {β : Type u} {α : Type v} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [inst : CommMonoid β] [inst : DecidableEq α] (h : Disjoint s₁ s₂) : (Finset.prod (s₁ ∪ s₂) fun x => f x) = (Finset.prod s₁ fun x => f x) * Finset.prod s₂ fun x => f x

ink

theorem Finset.sum_filter_add_sum_filter_not {β : Type u} {α : Type v} [inst : AddCommMonoid β] (s : Finset α) (p : α → Prop) [inst : DecidablePred p] [inst : (x : α) → Decidable ¬p x] (f : α → β) : ((Finset.sum (Finset.filter p s) fun x => f x) + Finset.sum (Finset.filter (fun x => ¬p x) s) fun x => f x) = Finset.sum s fun x => f x

ink

theorem Finset.prod_filter_mul_prod_filter_not {β : Type u} {α : Type v} [inst : CommMonoid β] (s : Finset α) (p : α → Prop) [inst : DecidablePred p] [inst : (x : α) → Decidable ¬p x] (f : α → β) : ((Finset.prod (Finset.filter p s) fun x => f x) * Finset.prod (Finset.filter (fun x => ¬p x) s) fun x => f x) = Finset.prod s fun x => f x

ink

@[simp]

theorem Finset.sum_to_list {β : Type u} {α : Type v} [inst : AddCommMonoid β] (s : Finset α) (f : α → β) : List.sum (List.map f (Finset.toList s)) = Finset.sum s f

ink

@[simp]

theorem Finset.prod_to_list {β : Type u} {α : Type v} [inst : CommMonoid β] (s : Finset α) (f : α → β) : List.prod (List.map f (Finset.toList s)) = Finset.prod s f

ink

theorem Equiv.Perm.sum_comp {β : Type u} {α : Type v} [inst : AddCommMonoid β] (σ : Equiv.Perm α) (s : Finset α) (f : α → β) (hs : { a | ↑σ a ≠ a } ⊆ ↑s) : (Finset.sum s fun x => f (↑σ x)) = Finset.sum s fun x => f x

ink

theorem Equiv.Perm.prod_comp {β : Type u} {α : Type v} [inst : CommMonoid β] (σ : Equiv.Perm α) (s : Finset α) (f : α → β) (hs : { a | ↑σ a ≠ a } ⊆ ↑s) : (Finset.prod s fun x => f (↑σ x)) = Finset.prod s fun x => f x

ink

theorem Equiv.Perm.sum_comp' {β : Type u} {α : Type v} [inst : AddCommMonoid β] (σ : Equiv.Perm α) (s : Finset α) (f : α → α → β) (hs : { a | ↑σ a ≠ a } ⊆ ↑s) : (Finset.sum s fun x => f (↑σ x) x) = Finset.sum s fun x => f x (↑(Equiv.symm σ) x)

ink

theorem Equiv.Perm.prod_comp' {β : Type u} {α : Type v} [inst : CommMonoid β] (σ : Equiv.Perm α) (s : Finset α) (f : α → α → β) (hs : { a | ↑σ a ≠ a } ⊆ ↑s) : (Finset.prod s fun x => f (↑σ x) x) = Finset.prod s fun x => f x (↑(Equiv.symm σ) x)

ink

theorem IsCompl.sum_add_sum {β : Type u} {α : Type v} [inst : Fintype α] [inst : AddCommMonoid β] {s : Finset α} {t : Finset α} (h : IsCompl s t) (f : α → β) : ((Finset.sum s fun i => f i) + Finset.sum t fun i => f i) = Finset.sum Finset.univ fun i => f i

ink

theorem IsCompl.prod_mul_prod {β : Type u} {α : Type v} [inst : Fintype α] [inst : CommMonoid β] {s : Finset α} {t : Finset α} (h : IsCompl s t) (f : α → β) : ((Finset.prod s fun i => f i) * Finset.prod t fun i => f i) = Finset.prod Finset.univ fun i => f i

ink

theorem Finset.sum_add_sum_compl {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : Fintype α] [inst : DecidableEq α] (s : Finset α) (f : α → β) : ((Finset.sum s fun i => f i) + Finset.sum (sᶜ) fun i => f i) = Finset.sum Finset.univ fun 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.

ink

theorem Finset.prod_mul_prod_compl {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : Fintype α] [inst : DecidableEq α] (s : Finset α) (f : α → β) : ((Finset.prod s fun i => f i) * Finset.prod (sᶜ) fun i => f i) = Finset.prod Finset.univ fun 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.

ink

theorem Finset.sum_compl_add_sum {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : Fintype α] [inst : DecidableEq α] (s : Finset α) (f : α → β) : ((Finset.sum (sᶜ) fun i => f i) + Finset.sum s fun i => f i) = Finset.sum Finset.univ fun i => f i

ink

theorem Finset.prod_compl_mul_prod {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : Fintype α] [inst : DecidableEq α] (s : Finset α) (f : α → β) : ((Finset.prod (sᶜ) fun i => f i) * Finset.prod s fun i => f i) = Finset.prod Finset.univ fun i => f i

ink

theorem Finset.sum_sdiff {β : Type u} {α : Type v} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [inst : AddCommMonoid β] [inst : DecidableEq α] (h : s₁ ⊆ s₂) : ((Finset.sum (s₂ \ s₁) fun x => f x) + Finset.sum s₁ fun x => f x) = Finset.sum s₂ fun x => f x

ink

theorem Finset.prod_sdiff {β : Type u} {α : Type v} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [inst : CommMonoid β] [inst : DecidableEq α] (h : s₁ ⊆ s₂) : ((Finset.prod (s₂ \ s₁) fun x => f x) * Finset.prod s₁ fun x => f x) = Finset.prod s₂ fun x => f x

ink

@[simp]

theorem Finset.sum_disj_sum {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] (s : Finset α) (t : Finset γ) (f : α ⊕ γ → β) : (Finset.sum (Finset.disjSum s t) fun x => f x) = (Finset.sum s fun x => f (Sum.inl x)) + Finset.sum t fun x => f (Sum.inr x)

ink

@[simp]

theorem Finset.prod_disj_sum {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] (s : Finset α) (t : Finset γ) (f : α ⊕ γ → β) : (Finset.prod (Finset.disjSum s t) fun x => f x) = (Finset.prod s fun x => f (Sum.inl x)) * Finset.prod t fun x => f (Sum.inr x)

ink

theorem Finset.sum_sum_elim {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] (s : Finset α) (t : Finset γ) (f : α → β) (g : γ → β) : (Finset.sum (Finset.disjSum s t) fun x => Sum.elim f g x) = (Finset.sum s fun x => f x) + Finset.sum t fun x => g x

ink

theorem Finset.prod_sum_elim {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] (s : Finset α) (t : Finset γ) (f : α → β) (g : γ → β) : (Finset.prod (Finset.disjSum s t) fun x => Sum.elim f g x) = (Finset.prod s fun x => f x) * Finset.prod t fun x => g x

ink

theorem Finset.sum_bunionᵢ {β : Type u} {α : Type v} {γ : Type w} {f : α → β} [inst : AddCommMonoid β] [inst : DecidableEq α] {s : Finset γ} {t : γ → Finset α} (hs : Set.PairwiseDisjoint (↑s) t) : (Finset.sum (Finset.bunionᵢ s t) fun x => f x) = Finset.sum s fun x => Finset.sum (t x) fun i => f i

ink

theorem Finset.prod_bunionᵢ {β : Type u} {α : Type v} {γ : Type w} {f : α → β} [inst : CommMonoid β] [inst : DecidableEq α] {s : Finset γ} {t : γ → Finset α} (hs : Set.PairwiseDisjoint (↑s) t) : (Finset.prod (Finset.bunionᵢ s t) fun x => f x) = Finset.prod s fun x => Finset.prod (t x) fun i => f i

ink

theorem Finset.sum_sigma {β : Type u} {α : Type v} [inst : AddCommMonoid β] {σ : α → Type u_1} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : Sigma σ → β) : (Finset.sum (Finset.sigma s t) fun x => f x) = Finset.sum s fun a => Finset.sum (t a) fun s => f { fst := a, snd := s }

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

ink

theorem Finset.prod_sigma {β : Type u} {α : Type v} [inst : CommMonoid β] {σ : α → Type u_1} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : Sigma σ → β) : (Finset.prod (Finset.sigma s t) fun x => f x) = Finset.prod s fun a => Finset.prod (t a) fun s => f { fst := a, snd := s }

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

ink

theorem Finset.sum_sigma' {β : Type u} {α : Type v} [inst : AddCommMonoid β] {σ : α → Type u_1} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : (a : α) → σ a → β) : (Finset.sum s fun a => Finset.sum (t a) fun s => f a s) = Finset.sum (Finset.sigma s t) fun x => f x.fst x.snd

ink

theorem Finset.prod_sigma' {β : Type u} {α : Type v} [inst : CommMonoid β] {σ : α → Type u_1} (s : Finset α) (t : (a : α) → Finset (σ a)) (f : (a : α) → σ a → β) : (Finset.prod s fun a => Finset.prod (t a) fun s => f a s) = Finset.prod (Finset.sigma s t) fun x => f x.fst x.snd

ink

theorem Finset.sum_bij {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β} (i : (a : α) → a ∈ s → γ) (hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t) (h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)) (i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀ (b : γ), b ∈ t → ∃ a ha, b = i a ha) : (Finset.sum s fun x => f x) = Finset.sum t fun x => g x

Reorder a sum.

The difference with sum_bij' is that the bijection is specified as a surjective injection, rather than by an inverse function.

ink

theorem Finset.prod_bij {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β} (i : (a : α) → a ∈ s → γ) (hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t) (h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)) (i_inj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) (i_surj : ∀ (b : γ), b ∈ t → ∃ a ha, b = i a ha) : (Finset.prod s fun x => f x) = Finset.prod t fun x => g x

Reorder a product.

The difference with prod_bij' is that the bijection is specified as a surjective injection, rather than by an inverse function.

ink

theorem Finset.sum_bij' {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β} (i : (a : α) → a ∈ s → γ) (hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t) (h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)) (j : (a : γ) → a ∈ t → α) (hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s) (left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (hi a ha) = a) (right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (hj a ha) = a) : (Finset.sum s fun x => f x) = Finset.sum t fun x => g x

Reorder a sum.

The difference with sum_bij is that the bijection is specified with an inverse, rather than as a surjective injection.

ink

theorem Finset.prod_bij' {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] {s : Finset α} {t : Finset γ} {f : α → β} {g : γ → β} (i : (a : α) → a ∈ s → γ) (hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t) (h : ∀ (a : α) (ha : a ∈ s), f a = g (i a ha)) (j : (a : γ) → a ∈ t → α) (hj : ∀ (a : γ) (ha : a ∈ t), j a ha ∈ s) (left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) (hi a ha) = a) (right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) (hj a ha) = a) : (Finset.prod s fun x => f x) = Finset.prod t fun x => g x

Reorder a product.

The difference with prod_bij is that the bijection is specified with an inverse, rather than as a surjective injection.

ink

theorem Finset.Equiv.sum_comp_finset {ι : Type u_2} {β : Type u} [inst : AddCommMonoid β] {ι' : Type u_1} [inst : DecidableEq ι] (e : ι ≃ ι') (f : ι' → β) {s' : Finset ι'} {s : Finset ι} (h : s = Finset.image (↑(Equiv.symm e)) s') : (Finset.sum s' fun i' => f i') = Finset.sum s fun i => f (↑e i)

Reindexing a sum over a finset along an equivalence. See Equiv.sum_comp for the version where s and s' are univ.

ink

theorem Finset.Equiv.prod_comp_finset {ι : Type u_2} {β : Type u} [inst : CommMonoid β] {ι' : Type u_1} [inst : DecidableEq ι] (e : ι ≃ ι') (f : ι' → β) {s' : Finset ι'} {s : Finset ι} (h : s = Finset.image (↑(Equiv.symm e)) s') : (Finset.prod s' fun i' => f i') = Finset.prod s fun i => f (↑e i)

Reindexing a product over a finset along an equivalence. See Equiv.prod_comp for the version where s and s' are univ.

ink

theorem Finset.sum_finset_product {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst) {f : γ × α → β} : (Finset.sum r fun p => f p) = Finset.sum s fun c => Finset.sum (t c) fun a => f (c, a)

ink

theorem Finset.prod_finset_product {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst) {f : γ × α → β} : (Finset.prod r fun p => f p) = Finset.prod s fun c => Finset.prod (t c) fun a => f (c, a)

ink

theorem Finset.sum_finset_product' {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst) {f : γ → α → β} : (Finset.sum r fun p => f p.fst p.snd) = Finset.sum s fun c => Finset.sum (t c) fun a => f c a

ink

theorem Finset.prod_finset_product' {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] (r : Finset (γ × α)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : γ × α), p ∈ r ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst) {f : γ → α → β} : (Finset.prod r fun p => f p.fst p.snd) = Finset.prod s fun c => Finset.prod (t c) fun a => f c a

ink

theorem Finset.sum_finset_product_right {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.snd ∈ s ∧ p.fst ∈ t p.snd) {f : α × γ → β} : (Finset.sum r fun p => f p) = Finset.sum s fun c => Finset.sum (t c) fun a => f (a, c)

ink

theorem Finset.prod_finset_product_right {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.snd ∈ s ∧ p.fst ∈ t p.snd) {f : α × γ → β} : (Finset.prod r fun p => f p) = Finset.prod s fun c => Finset.prod (t c) fun a => f (a, c)

ink

theorem Finset.sum_finset_product_right' {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.snd ∈ s ∧ p.fst ∈ t p.snd) {f : α → γ → β} : (Finset.sum r fun p => f p.fst p.snd) = Finset.sum s fun c => Finset.sum (t c) fun a => f a c

ink

theorem Finset.prod_finset_product_right' {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] (r : Finset (α × γ)) (s : Finset γ) (t : γ → Finset α) (h : ∀ (p : α × γ), p ∈ r ↔ p.snd ∈ s ∧ p.fst ∈ t p.snd) {f : α → γ → β} : (Finset.prod r fun p => f p.fst p.snd) = Finset.prod s fun c => Finset.prod (t c) fun a => f a c

ink

theorem Finset.sum_fiberwise_of_maps_to {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] [inst : DecidableEq γ] {s : Finset α} {t : Finset γ} {g : α → γ} (h : ∀ (x : α), x ∈ s → g x ∈ t) (f : α → β) : (Finset.sum t fun y => Finset.sum (Finset.filter (fun x => g x = y) s) fun x => f x) = Finset.sum s fun x => f x

ink

theorem Finset.prod_fiberwise_of_maps_to {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] [inst : DecidableEq γ] {s : Finset α} {t : Finset γ} {g : α → γ} (h : ∀ (x : α), x ∈ s → g x ∈ t) (f : α → β) : (Finset.prod t fun y => Finset.prod (Finset.filter (fun x => g x = y) s) fun x => f x) = Finset.prod s fun x => f x

ink

abbrev Finset.sum_image'.match_1 {α : Type u_2} {γ : Type u_1} {s : Finset γ} {g : γ → α} (_x : α) (motive : (∃ a, a ∈ s ∧ g a = _x) → Prop) : (x : ∃ a, a ∈ s ∧ g a = _x) → ((c : γ) → (hcs : c ∈ s) → (hc : g c = _x) → motive (_ : ∃ a, a ∈ s ∧ g a = _x)) → motive x

Equations

• Finset.sum_image'.match_1 _x motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

ink

theorem Finset.sum_image' {β : Type u} {α : Type v} {γ : Type w} {f : α → β} [inst : AddCommMonoid β] [inst : DecidableEq α] {s : Finset γ} {g : γ → α} (h : γ → β) (eq : ∀ (c : γ), c ∈ s → f (g c) = Finset.sum (Finset.filter (fun c' => g c' = g c) s) fun x => h x) : (Finset.sum (Finset.image g s) fun x => f x) = Finset.sum s fun x => h x

ink

theorem Finset.prod_image' {β : Type u} {α : Type v} {γ : Type w} {f : α → β} [inst : CommMonoid β] [inst : DecidableEq α] {s : Finset γ} {g : γ → α} (h : γ → β) (eq : ∀ (c : γ), c ∈ s → f (g c) = Finset.prod (Finset.filter (fun c' => g c' = g c) s) fun x => h x) : (Finset.prod (Finset.image g s) fun x => f x) = Finset.prod s fun x => h x

ink

theorem Finset.sum_add_distrib {β : Type u} {α : Type v} {s : Finset α} {f : α → β} {g : α → β} [inst : AddCommMonoid β] : (Finset.sum s fun x => f x + g x) = (Finset.sum s fun x => f x) + Finset.sum s fun x => g x

ink

theorem Finset.prod_mul_distrib {β : Type u} {α : Type v} {s : Finset α} {f : α → β} {g : α → β} [inst : CommMonoid β] : (Finset.prod s fun x => f x * g x) = (Finset.prod s fun x => f x) * Finset.prod s fun x => g x

ink

theorem Finset.sum_product {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] {s : Finset γ} {t : Finset α} {f : γ × α → β} : (Finset.sum (s ×ᶠ t) fun x => f x) = Finset.sum s fun x => Finset.sum t fun y => f (x, y)

ink

theorem Finset.prod_product {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ × α → β} : (Finset.prod (s ×ᶠ t) fun x => f x) = Finset.prod s fun x => Finset.prod t fun y => f (x, y)

ink

theorem Finset.sum_product' {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} : (Finset.sum (s ×ᶠ t) fun x => f x.fst x.snd) = Finset.sum s fun x => Finset.sum t fun y => f x y

An uncurried version of Finset.sum_product

ink

theorem Finset.prod_product' {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} : (Finset.prod (s ×ᶠ t) fun x => f x.fst x.snd) = Finset.prod s fun x => Finset.prod t fun y => f x y

An uncurried version of Finset.prod_product.

ink

theorem Finset.sum_product_right {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] {s : Finset γ} {t : Finset α} {f : γ × α → β} : (Finset.sum (s ×ᶠ t) fun x => f x) = Finset.sum t fun y => Finset.sum s fun x => f (x, y)

ink

theorem Finset.prod_product_right {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ × α → β} : (Finset.prod (s ×ᶠ t) fun x => f x) = Finset.prod t fun y => Finset.prod s fun x => f (x, y)

ink

theorem Finset.sum_product_right' {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} : (Finset.sum (s ×ᶠ t) fun x => f x.fst x.snd) = Finset.sum t fun y => Finset.sum s fun x => f x y

An uncurried version of Finset.prod_product_right

ink

theorem Finset.prod_product_right' {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} : (Finset.prod (s ×ᶠ t) fun x => f x.fst x.snd) = Finset.prod t fun y => Finset.prod s fun x => f x y

An uncurried version of Finset.prod_product_right.

ink

abbrev Finset.sum_comm'.match_1 {α : Type u_2} {γ : Type u_1} (motive : γ × α → Prop) : (x : γ × α) → ((x : γ) → (y : α) → motive (x, y)) → motive x

Equations

• Finset.sum_comm'.match_1 motive x h_1 = Prod.casesOn x fun fst snd => h_1 fst snd

ink

theorem Finset.sum_comm' {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] {s : Finset γ} {t : γ → Finset α} {t' : Finset α} {s' : α → Finset γ} (h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') {f : γ → α → β} : (Finset.sum s fun x => Finset.sum (t x) fun y => f x y) = Finset.sum t' fun y => Finset.sum (s' y) fun x => f x y

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

ink

theorem Finset.prod_comm' {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] {s : Finset γ} {t : γ → Finset α} {t' : Finset α} {s' : α → Finset γ} (h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t') {f : γ → α → β} : (Finset.prod s fun x => Finset.prod (t x) fun y => f x y) = Finset.prod t' fun y => Finset.prod (s' y) fun x => f x y

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

ink

theorem Finset.sum_comm {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} : (Finset.sum s fun x => Finset.sum t fun y => f x y) = Finset.sum t fun y => Finset.sum s fun x => f x y

ink

theorem Finset.prod_comm {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] {s : Finset γ} {t : Finset α} {f : γ → α → β} : (Finset.prod s fun x => Finset.prod t fun y => f x y) = Finset.prod t fun y => Finset.prod s fun x => f x y

ink

theorem Finset.sum_hom_rel {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] [inst : AddCommMonoid γ] {r : β → γ → Prop} {f : α → β} {g : α → γ} {s : Finset α} (h₁ : r 0 0) (h₂ : (a : α) → (b : β) → (c : γ) → r b c → r (f a + b) (g a + c)) : r (Finset.sum s fun x => f x) (Finset.sum s fun x => g x)

ink

theorem Finset.prod_hom_rel {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] [inst : CommMonoid γ] {r : β → γ → Prop} {f : α → β} {g : α → γ} {s : Finset α} (h₁ : r 1 1) (h₂ : (a : α) → (b : β) → (c : γ) → r b c → r (f a * b) (g a * c)) : r (Finset.prod s fun x => f x) (Finset.prod s fun x => g x)

ink

theorem Finset.sum_eq_zero {β : Type u} {α : Type v} [inst : AddCommMonoid β] {f : α → β} {s : Finset α} (h : ∀ (x : α), x ∈ s → f x = 0) : (Finset.sum s fun x => f x) = 0

ink

theorem Finset.prod_eq_one {β : Type u} {α : Type v} [inst : CommMonoid β] {f : α → β} {s : Finset α} (h : ∀ (x : α), x ∈ s → f x = 1) : (Finset.prod s fun x => f x) = 1

ink

theorem Finset.sum_subset_zero_on_sdiff {β : Type u} {α : Type v} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} {g : α → β} [inst : AddCommMonoid β] [inst : DecidableEq α] (h : s₁ ⊆ s₂) (hg : ∀ (x : α), x ∈ s₂ \ s₁ → g x = 0) (hfg : ∀ (x : α), x ∈ s₁ → f x = g x) : (Finset.sum s₁ fun i => f i) = Finset.sum s₂ fun i => g i

ink

theorem Finset.prod_subset_one_on_sdiff {β : Type u} {α : Type v} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} {g : α → β} [inst : CommMonoid β] [inst : DecidableEq α] (h : s₁ ⊆ s₂) (hg : ∀ (x : α), x ∈ s₂ \ s₁ → g x = 1) (hfg : ∀ (x : α), x ∈ s₁ → f x = g x) : (Finset.prod s₁ fun i => f i) = Finset.prod s₂ fun i => g i

ink

theorem Finset.sum_subset {β : Type u} {α : Type v} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [inst : AddCommMonoid β] (h : s₁ ⊆ s₂) (hf : ∀ (x : α), x ∈ s₂ → ¬x ∈ s₁ → f x = 0) : (Finset.sum s₁ fun x => f x) = Finset.sum s₂ fun x => f x

ink

theorem Finset.prod_subset {β : Type u} {α : Type v} {s₁ : Finset α} {s₂ : Finset α} {f : α → β} [inst : CommMonoid β] (h : s₁ ⊆ s₂) (hf : ∀ (x : α), x ∈ s₂ → ¬x ∈ s₁ → f x = 1) : (Finset.prod s₁ fun x => f x) = Finset.prod s₂ fun x => f x

ink

theorem Finset.sum_filter_of_ne {β : Type u} {α : Type v} {s : Finset α} {f : α → β} [inst : AddCommMonoid β] {p : α → Prop} [inst : DecidablePred p] (hp : (x : α) → x ∈ s → f x ≠ 0 → p x) : (Finset.sum (Finset.filter p s) fun x => f x) = Finset.sum s fun x => f x

ink

theorem Finset.prod_filter_of_ne {β : Type u} {α : Type v} {s : Finset α} {f : α → β} [inst : CommMonoid β] {p : α → Prop} [inst : DecidablePred p] (hp : (x : α) → x ∈ s → f x ≠ 1 → p x) : (Finset.prod (Finset.filter p s) fun x => f x) = Finset.prod s fun x => f x

ink

theorem Finset.sum_filter_ne_zero {β : Type u} {α : Type v} {s : Finset α} {f : α → β} [inst : AddCommMonoid β] [inst : (x : α) → Decidable (f x ≠ 0)] : (Finset.sum (Finset.filter (fun x => f x ≠ 0) s) fun x => f x) = Finset.sum s fun x => f x

ink

theorem Finset.prod_filter_ne_one {β : Type u} {α : Type v} {s : Finset α} {f : α → β} [inst : CommMonoid β] [inst : (x : α) → Decidable (f x ≠ 1)] : (Finset.prod (Finset.filter (fun x => f x ≠ 1) s) fun x => f x) = Finset.prod s fun x => f x

ink

theorem Finset.sum_filter {β : Type u} {α : Type v} {s : Finset α} [inst : AddCommMonoid β] (p : α → Prop) [inst : DecidablePred p] (f : α → β) : (Finset.sum (Finset.filter p s) fun a => f a) = Finset.sum s fun a => if p a then f a else 0

ink

theorem Finset.prod_filter {β : Type u} {α : Type v} {s : Finset α} [inst : CommMonoid β] (p : α → Prop) [inst : DecidablePred p] (f : α → β) : (Finset.prod (Finset.filter p s) fun a => f a) = Finset.prod s fun a => if p a then f a else 1

ink

theorem Finset.sum_eq_single_of_mem {β : Type u} {α : Type v} [inst : AddCommMonoid β] {s : Finset α} {f : α → β} (a : α) (h : a ∈ s) (h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 0) : (Finset.sum s fun x => f x) = f a

ink

theorem Finset.prod_eq_single_of_mem {β : Type u} {α : Type v} [inst : CommMonoid β] {s : Finset α} {f : α → β} (a : α) (h : a ∈ s) (h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 1) : (Finset.prod s fun x => f x) = f a

ink

theorem Finset.sum_eq_single {β : Type u} {α : Type v} [inst : AddCommMonoid β] {s : Finset α} {f : α → β} (a : α) (h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 0) (h₁ : ¬a ∈ s → f a = 0) : (Finset.sum s fun x => f x) = f a

ink

abbrev Finset.sum_eq_single.match_1 {α : Type u_1} {s : Finset α} (a : α) (motive : ¬a ∈ s → Prop) : (x : ¬a ∈ s) → ((this : ¬a ∈ s) → motive this) → motive x

Equations

• Finset.sum_eq_single.match_1 a motive x h_1 = h_1 x

ink

theorem Finset.prod_eq_single {β : Type u} {α : Type v} [inst : CommMonoid β] {s : Finset α} {f : α → β} (a : α) (h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 1) (h₁ : ¬a ∈ s → f a = 1) : (Finset.prod s fun x => f x) = f a

ink

theorem Finset.sum_eq_add_of_mem {β : Type u} {α : Type v} [inst : AddCommMonoid β] {s : Finset α} {f : α → β} (a : α) (b : α) (ha : a ∈ s) (hb : b ∈ s) (hn : a ≠ b) (h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 0) : (Finset.sum s fun x => f x) = f a + f b

ink

theorem Finset.prod_eq_mul_of_mem {β : Type u} {α : Type v} [inst : CommMonoid β] {s : Finset α} {f : α → β} (a : α) (b : α) (ha : a ∈ s) (hb : b ∈ s) (hn : a ≠ b) (h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1) : (Finset.prod s fun x => f x) = f a * f b

ink

theorem Finset.sum_eq_add {β : Type u} {α : Type v} [inst : AddCommMonoid β] {s : Finset α} {f : α → β} (a : α) (b : α) (hn : a ≠ b) (h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 0) (ha : ¬a ∈ s → f a = 0) (hb : ¬b ∈ s → f b = 0) : (Finset.sum s fun x => f x) = f a + f b

ink

theorem Finset.prod_eq_mul {β : Type u} {α : Type v} [inst : CommMonoid β] {s : Finset α} {f : α → β} (a : α) (b : α) (hn : a ≠ b) (h₀ : ∀ (c : α), c ∈ s → c ≠ a ∧ c ≠ b → f c = 1) (ha : ¬a ∈ s → f a = 1) (hb : ¬b ∈ s → f b = 1) : (Finset.prod s fun x => f x) = f a * f b

ink

theorem Finset.sum_attach {β : Type u} {α : Type v} {s : Finset α} [inst : AddCommMonoid β] {f : α → β} : (Finset.sum (Finset.attach s) fun x => f ↑x) = Finset.sum s fun x => f x

ink

theorem Finset.prod_attach {β : Type u} {α : Type v} {s : Finset α} [inst : CommMonoid β] {f : α → β} : (Finset.prod (Finset.attach s) fun x => f ↑x) = Finset.prod s fun x => f x

ink

@[simp]

theorem Finset.sum_subtype_eq_sum_filter {β : Type u} {α : Type v} {s : Finset α} [inst : AddCommMonoid β] (f : α → β) {p : α → Prop} [inst : DecidablePred p] : (Finset.sum (Finset.subtype p s) fun x => f ↑x) = Finset.sum (Finset.filter p s) fun x => f x

A sum over s.subtype p equals one over s.filter p.

ink

@[simp]

theorem Finset.prod_subtype_eq_prod_filter {β : Type u} {α : Type v} {s : Finset α} [inst : CommMonoid β] (f : α → β) {p : α → Prop} [inst : DecidablePred p] : (Finset.prod (Finset.subtype p s) fun x => f ↑x) = Finset.prod (Finset.filter p s) fun x => f x

A product over s.subtype p equals one over s.filter p.

ink

theorem Finset.sum_subtype_of_mem {β : Type u} {α : Type v} {s : Finset α} [inst : AddCommMonoid β] (f : α → β) {p : α → Prop} [inst : DecidablePred p] (h : (x : α) → x ∈ s → p x) : (Finset.sum (Finset.subtype p s) fun x => f ↑x) = Finset.sum s fun x => f x

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

ink

theorem Finset.prod_subtype_of_mem {β : Type u} {α : Type v} {s : Finset α} [inst : CommMonoid β] (f : α → β) {p : α → Prop} [inst : DecidablePred p] (h : (x : α) → x ∈ s → p x) : (Finset.prod (Finset.subtype p s) fun x => f ↑x) = Finset.prod s fun x => f x

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

ink

theorem Finset.sum_subtype_map_embedding {β : Type u} {α : Type v} [inst : AddCommMonoid β] {p : α → Prop} {s : Finset { x // p x }} {f : { x // p x } → β} {g : α → β} (h : ∀ (x : { x // p x }), x ∈ s → g ↑x = f x) : (Finset.sum (Finset.map (Function.Embedding.subtype fun x => p x) s) fun x => g x) = Finset.sum s fun x => 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.

ink

theorem Finset.prod_subtype_map_embedding {β : Type u} {α : Type v} [inst : CommMonoid β] {p : α → Prop} {s : Finset { x // p x }} {f : { x // p x } → β} {g : α → β} (h : ∀ (x : { x // p x }), x ∈ s → g ↑x = f x) : (Finset.prod (Finset.map (Function.Embedding.subtype fun x => p x) s) fun x => g x) = Finset.prod s fun x => 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.

ink

theorem Finset.sum_coe_sort_eq_attach {β : Type u} {α : Type v} (s : Finset α) [inst : AddCommMonoid β] (f : { x // x ∈ s } → β) : (Finset.sum Finset.univ fun i => f i) = Finset.sum (Finset.attach s) fun i => f i

ink

theorem Finset.prod_coe_sort_eq_attach {β : Type u} {α : Type v} (s : Finset α) [inst : CommMonoid β] (f : { x // x ∈ s } → β) : (Finset.prod Finset.univ fun i => f i) = Finset.prod (Finset.attach s) fun i => f i

ink

theorem Finset.sum_coe_sort {β : Type u} {α : Type v} (s : Finset α) (f : α → β) [inst : AddCommMonoid β] : (Finset.sum Finset.univ fun i => f ↑i) = Finset.sum s fun i => f i

ink

theorem Finset.prod_coe_sort {β : Type u} {α : Type v} (s : Finset α) (f : α → β) [inst : CommMonoid β] : (Finset.prod Finset.univ fun i => f ↑i) = Finset.prod s fun i => f i

ink

theorem Finset.sum_finset_coe {β : Type u} {α : Type v} [inst : AddCommMonoid β] (f : α → β) (s : Finset α) : (Finset.sum Finset.univ fun i => f ↑i) = Finset.sum s fun i => f i

ink

theorem Finset.prod_finset_coe {β : Type u} {α : Type v} [inst : CommMonoid β] (f : α → β) (s : Finset α) : (Finset.prod Finset.univ fun i => f ↑i) = Finset.prod s fun i => f i

ink

theorem Finset.sum_subtype {β : Type u} {α : Type v} [inst : AddCommMonoid β] {p : α → Prop} {F : Fintype (Subtype p)} (s : Finset α) (h : ∀ (x : α), x ∈ s ↔ p x) (f : α → β) : (Finset.sum s fun a => f a) = Finset.sum Finset.univ fun a => f ↑a

ink

theorem Finset.prod_subtype {β : Type u} {α : Type v} [inst : CommMonoid β] {p : α → Prop} {F : Fintype (Subtype p)} (s : Finset α) (h : ∀ (x : α), x ∈ s ↔ p x) (f : α → β) : (Finset.prod s fun a => f a) = Finset.prod Finset.univ fun a => f ↑a

ink

theorem Finset.sum_congr_set {α : Type u_1} [inst : AddCommMonoid α] {β : Type u_2} [inst : Fintype β] (s : Set β) [inst : DecidablePred fun x => x ∈ s] (f : β → α) (g : ↑s → α) (w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }) (w' : ∀ (x : β), ¬x ∈ s → f x = 0) : Finset.sum Finset.univ f = Finset.sum Finset.univ 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.

ink

abbrev Finset.sum_congr_set.match_1 {β : Type u_1} [inst : Fintype β] (s : Set β) [inst : DecidablePred fun x => x ∈ s] (motive : (x : { x // x ∈ s }) → x ∈ Finset.univ → Prop) : (x : { x // x ∈ s }) → (x_1 : x ∈ Finset.univ) → ((x : β) → (h : x ∈ s) → (x_2 : { val := x, property := h } ∈ Finset.univ) → motive { val := x, property := h } x_2) → motive x x_1

Equations

• Finset.sum_congr_set.match_1 s motive x x h_1 = Subtype.casesOn β (fun x => x ∈ s) (fun x => (x_1 : x ∈ Finset.univ) → motive x x_1) x (fun val property x => h_1 val property x) x

ink

theorem Finset.prod_congr_set {α : Type u_1} [inst : CommMonoid α] {β : Type u_2} [inst : Fintype β] (s : Set β) [inst : DecidablePred fun x => x ∈ s] (f : β → α) (g : ↑s → α) (w : ∀ (x : β) (h : x ∈ s), f x = g { val := x, property := h }) (w' : ∀ (x : β), ¬x ∈ s → f x = 1) : Finset.prod Finset.univ f = Finset.prod Finset.univ 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.

ink

theorem Finset.sum_apply_dite {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} [inst : DecidablePred fun x => ¬p x] (f : (x : α) → p x → γ) (g : (x : α) → ¬p x → γ) (h : γ → β) : (Finset.sum s fun x => h (if hx : p x then f x hx else g x hx)) = (Finset.sum (Finset.attach (Finset.filter p s)) fun x => h (f ↑x (_ : ↑x ∈ s ∧ p ↑x).right)) + Finset.sum (Finset.attach (Finset.filter (fun x => ¬p x) s)) fun x => h (g ↑x (_ : ¬p ↑x))

ink

theorem Finset.prod_apply_dite {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} [inst : DecidablePred fun x => ¬p x] (f : (x : α) → p x → γ) (g : (x : α) → ¬p x → γ) (h : γ → β) : (Finset.prod s fun x => h (if hx : p x then f x hx else g x hx)) = (Finset.prod (Finset.attach (Finset.filter p s)) fun x => h (f ↑x (_ : ↑x ∈ s ∧ p ↑x).right)) * Finset.prod (Finset.attach (Finset.filter (fun x => ¬p x) s)) fun x => h (g ↑x (_ : ¬p ↑x))

ink

theorem Finset.sum_apply_ite {β : Type u} {α : Type v} {γ : Type w} [inst : AddCommMonoid β] {s : Finset α} {p : α → Prop} {_hp : DecidablePred p} (f : α → γ) (g : α → γ) (h : γ → β) : (Finset.sum s fun x => h (if p x then f x else g x)) = (Finset.sum (Finset.filter p s) fun x => h (f x)) + Finset.sum (Finset.filter (fun x => ¬p x) s) fun x => h (g x)

ink

theorem Finset.prod_apply_ite {β : Type u} {α : Type v} {γ : Type w} [inst : CommMonoid β] {s : Finset α} {p : α → Prop} {_hp : DecidablePred p} (f : α → γ) (g : α → γ) (h : γ → β) : (Finset.prod s fun x => h (if p x then f x else g x)) = (Finset.prod (Finset.filter p s) fun x => h (f x)) * Finset.prod (Finset.filter (fun x => ¬p x) s) fun x => h (g x)

ink

theorem Finset.sum_dite {β : Type u} {α : Type v} [inst : AddCommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (Finset.sum s fun x => if hx : p x then f x hx else g x hx) = (Finset.sum (Finset.attach (Finset.filter p s)) fun x => f ↑x (_ : ↑x ∈ s ∧ p ↑x).right) + Finset.sum (Finset.attach (Finset.filter (fun x => ¬p x) s)) fun x => g ↑x (_ : ¬p ↑x)

ink

theorem Finset.prod_dite {β : Type u} {α : Type v} [inst : CommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (Finset.prod s fun x => if hx : p x then f x hx else g x hx) = (Finset.prod (Finset.attach (Finset.filter p s)) fun x => f ↑x (_ : ↑x ∈ s ∧ p ↑x).right) * Finset.prod (Finset.attach (Finset.filter (fun x => ¬p x) s)) fun x => g ↑x (_ : ¬p ↑x)

ink

theorem Finset.sum_ite {β : Type u} {α : Type v} [inst : AddCommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : α → β) (g : α → β) : (Finset.sum s fun x => if p x then f x else g x) = (Finset.sum (Finset.filter p s) fun x => f x) + Finset.sum (Finset.filter (fun x => ¬p x) s) fun x => g x

ink

theorem Finset.prod_ite {β : Type u} {α : Type v} [inst : CommMonoid β] {s : Finset α} {p : α → Prop} {hp : DecidablePred p} (f : α → β) (g : α → β) : (Finset.prod s fun x => if p x then f x else g x) = (Finset.prod (Finset.filter p s) fun x => f x) * Finset.prod (Finset.filter (fun x => ¬p x) s) fun x => g x

ink

theorem Finset.sum_ite_of_false {β : Type u} {α : Type v} {s : Finset α} [inst : AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → β) (g : α → β) (h : ∀ (x : α), x ∈ s → ¬p x) : (Finset.sum s fun x => if p x then f x else g x) = Finset.sum s fun x => g x

ink

theorem Finset.prod_ite_of_false {β : Type u} {α : Type v} {s : Finset α} [inst : CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → β) (g : α → β) (h : ∀ (x : α), x ∈ s → ¬p x) : (Finset.prod s fun x => if p x then f x else g x) = Finset.prod s fun x => g x

ink

theorem Finset.sum_ite_of_true {β : Type u} {α : Type v} {s : Finset α} [inst : AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → β) (g : α → β) (h : (x : α) → x ∈ s → p x) : (Finset.sum s fun x => if p x then f x else g x) = Finset.sum s fun x => f x

ink

theorem Finset.prod_ite_of_true {β : Type u} {α : Type v} {s : Finset α} [inst : CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → β) (g : α → β) (h : (x : α) → x ∈ s → p x) : (Finset.prod s fun x => if p x then f x else g x) = Finset.prod s fun x => f x

ink

theorem Finset.sum_apply_ite_of_false {β : Type u} {α : Type v} {γ : Type w} {s : Finset α} [inst : AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → γ) (g : α → γ) (k : γ → β) (h : ∀ (x : α), x ∈ s → ¬p x) : (Finset.sum s fun x => k (if p x then f x else g x)) = Finset.sum s fun x => k (g x)

ink

theorem Finset.prod_apply_ite_of_false {β : Type u} {α : Type v} {γ : Type w} {s : Finset α} [inst : CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → γ) (g : α → γ) (k : γ → β) (h : ∀ (x : α), x ∈ s → ¬p x) : (Finset.prod s fun x => k (if p x then f x else g x)) = Finset.prod s fun x => k (g x)

ink

theorem Finset.sum_apply_ite_of_true {β : Type u} {α : Type v} {γ : Type w} {s : Finset α} [inst : AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → γ) (g : α → γ) (k : γ → β) (h : (x : α) → x ∈ s → p x) : (Finset.sum s fun x => k (if p x then f x else g x)) = Finset.sum s fun x => k (f x)

ink

theorem Finset.prod_apply_ite_of_true {β : Type u} {α : Type v} {γ : Type w} {s : Finset α} [inst : CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (f : α → γ) (g : α → γ) (k : γ → β) (h : (x : α) → x ∈ s → p x) : (Finset.prod s fun x => k (if p x then f x else g x)) = Finset.prod s fun x => k (f x)

ink

theorem Finset.sum_extend_by_zero {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (f : α → β) : (Finset.sum s fun i => if i ∈ s then f i else 0) = Finset.sum s fun i => f i

ink

theorem Finset.prod_extend_by_one {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (f : α → β) : (Finset.prod s fun i => if i ∈ s then f i else 1) = Finset.prod s fun i => f i

ink

@[simp]

theorem Finset.sum_ite_mem {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (t : Finset α) (f : α → β) : (Finset.sum s fun i => if i ∈ t then f i else 0) = Finset.sum (s ∩ t) fun i => f i

ink

@[simp]

theorem Finset.prod_ite_mem {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (t : Finset α) (f : α → β) : (Finset.prod s fun i => if i ∈ t then f i else 1) = Finset.prod (s ∩ t) fun i => f i

ink

@[simp]

theorem Finset.sum_dite_eq {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → a = x → β) : (Finset.sum s fun x => if h : a = x then b x h else 0) = if a ∈ s then b a (_ : a = a) else 0

ink

@[simp]

theorem Finset.prod_dite_eq {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → a = x → β) : (Finset.prod s fun x => if h : a = x then b x h else 1) = if a ∈ s then b a (_ : a = a) else 1

ink

@[simp]

theorem Finset.sum_dite_eq' {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → x = a → β) : (Finset.sum s fun x => if h : x = a then b x h else 0) = if a ∈ s then b a (_ : a = a) else 0

ink

@[simp]

theorem Finset.prod_dite_eq' {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (a : α) (b : (x : α) → x = a → β) : (Finset.prod s fun x => if h : x = a then b x h else 1) = if a ∈ s then b a (_ : a = a) else 1

ink

@[simp]

theorem Finset.sum_ite_eq {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (Finset.sum s fun x => if a = x then b x else 0) = if a ∈ s then b a else 0

ink

@[simp]

theorem Finset.prod_ite_eq {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (Finset.prod s fun x => if a = x then b x else 1) = if a ∈ s then b a else 1

ink

@[simp]

theorem Finset.sum_ite_eq' {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (Finset.sum s fun x => 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.

ink

@[simp]

theorem Finset.prod_ite_eq' {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (a : α) (b : α → β) : (Finset.prod s fun x => 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.

ink

theorem Finset.sum_ite_index {β : Type u} {α : Type v} [inst : AddCommMonoid β] (p : Prop) [inst : Decidable p] (s : Finset α) (t : Finset α) (f : α → β) : (Finset.sum (if p then s else t) fun x => f x) = if p then Finset.sum s fun x => f x else Finset.sum t fun x => f x

ink

theorem Finset.prod_ite_index {β : Type u} {α : Type v} [inst : CommMonoid β] (p : Prop) [inst : Decidable p] (s : Finset α) (t : Finset α) (f : α → β) : (Finset.prod (if p then s else t) fun x => f x) = if p then Finset.prod s fun x => f x else Finset.prod t fun x => f x

ink

@[simp]

theorem Finset.sum_ite_irrel {β : Type u} {α : Type v} [inst : AddCommMonoid β] (p : Prop) [inst : Decidable p] (s : Finset α) (f : α → β) (g : α → β) : (Finset.sum s fun x => if p then f x else g x) = if p then Finset.sum s fun x => f x else Finset.sum s fun x => g x

ink

@[simp]

theorem Finset.prod_ite_irrel {β : Type u} {α : Type v} [inst : CommMonoid β] (p : Prop) [inst : Decidable p] (s : Finset α) (f : α → β) (g : α → β) : (Finset.prod s fun x => if p then f x else g x) = if p then Finset.prod s fun x => f x else Finset.prod s fun x => g x

ink

@[simp]

theorem Finset.sum_dite_irrel {β : Type u} {α : Type v} [inst : AddCommMonoid β] (p : Prop) [inst : Decidable p] (s : Finset α) (f : p → α → β) (g : ¬p → α → β) : (Finset.sum s fun x => if h : p then f h x else g h x) = if h : p then Finset.sum s fun x => f h x else Finset.sum s fun x => g h x

ink

@[simp]

theorem Finset.prod_dite_irrel {β : Type u} {α : Type v} [inst : CommMonoid β] (p : Prop) [inst : Decidable p] (s : Finset α) (f : p → α → β) (g : ¬p → α → β) : (Finset.prod s fun x => if h : p then f h x else g h x) = if h : p then Finset.prod s fun x => f h x else Finset.prod s fun x => g h x

ink

@[simp]

theorem Finset.sum_pi_single' {ι : Type u_1} {M : Type u_2} [inst : DecidableEq ι] [inst : AddCommMonoid M] (i : ι) (x : M) (s : Finset ι) : (Finset.sum s fun j => Pi.single i x j) = if i ∈ s then x else 0

ink

@[simp]

theorem Finset.sum_pi_single {ι : Type u_1} {M : ι → Type u_2} [inst : DecidableEq ι] [inst : (i : ι) → AddCommMonoid (M i)] (i : ι) (f : (i : ι) → M i) (s : Finset ι) : (Finset.sum s fun j => Pi.single j (f j) i) = if i ∈ s then f i else 0

ink

theorem Finset.sum_bij_ne_zero {β : Type u} {α : Type v} {γ : Type w} [inst : 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₁ a₂ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 0) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 0), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂) (i_surj : ∀ (b : γ), b ∈ t → g b ≠ 0 → ∃ a h₁ h₂, b = i a h₁ h₂) (h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), f a = g (i a h₁ h₂)) : (Finset.sum s fun x => f x) = Finset.sum t fun x => g x

ink

theorem Finset.prod_bij_ne_one {β : Type u} {α : Type v} {γ : Type w} [inst : 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₁ a₂ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1), i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂) (i_surj : ∀ (b : γ), b ∈ t → g b ≠ 1 → ∃ a h₁ h₂, b = i a h₁ h₂) (h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)) : (Finset.prod s fun x => f x) = Finset.prod t fun x => g x

ink

theorem Finset.sum_dite_of_false {β : Type u} {α : Type v} {s : Finset α} [inst : AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (h : ∀ (x : α), x ∈ s → ¬p x) (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (Finset.sum s fun x => if hx : p x then f x hx else g x hx) = Finset.sum Finset.univ fun x => g (↑x) (h ↑x (_ : ↑x ∈ s))

ink

theorem Finset.prod_dite_of_false {β : Type u} {α : Type v} {s : Finset α} [inst : CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (h : ∀ (x : α), x ∈ s → ¬p x) (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (Finset.prod s fun x => if hx : p x then f x hx else g x hx) = Finset.prod Finset.univ fun x => g (↑x) (h ↑x (_ : ↑x ∈ s))

ink

theorem Finset.sum_dite_of_true {β : Type u} {α : Type v} {s : Finset α} [inst : AddCommMonoid β] {p : α → Prop} {hp : DecidablePred p} (h : (x : α) → x ∈ s → p x) (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (Finset.sum s fun x => if hx : p x then f x hx else g x hx) = Finset.sum Finset.univ fun x => f (↑x) (h ↑x (_ : ↑x ∈ s))

ink

theorem Finset.prod_dite_of_true {β : Type u} {α : Type v} {s : Finset α} [inst : CommMonoid β] {p : α → Prop} {hp : DecidablePred p} (h : (x : α) → x ∈ s → p x) (f : (x : α) → p x → β) (g : (x : α) → ¬p x → β) : (Finset.prod s fun x => if hx : p x then f x hx else g x hx) = Finset.prod Finset.univ fun x => f (↑x) (h ↑x (_ : ↑x ∈ s))

ink

theorem Finset.nonempty_of_sum_ne_zero {β : Type u} {α : Type v} {s : Finset α} {f : α → β} [inst : AddCommMonoid β] (h : (Finset.sum s fun x => f x) ≠ 0) : Finset.Nonempty s

ink

theorem Finset.nonempty_of_prod_ne_one {β : Type u} {α : Type v} {s : Finset α} {f : α → β} [inst : CommMonoid β] (h : (Finset.prod s fun x => f x) ≠ 1) : Finset.Nonempty s

ink

theorem Finset.exists_ne_zero_of_sum_ne_zero {β : Type u} {α : Type v} {s : Finset α} {f : α → β} [inst : AddCommMonoid β] (h : (Finset.sum s fun x => f x) ≠ 0) : ∃ a, a ∈ s ∧ f a ≠ 0

ink

theorem Finset.exists_ne_one_of_prod_ne_one {β : Type u} {α : Type v} {s : Finset α} {f : α → β} [inst : CommMonoid β] (h : (Finset.prod s fun x => f x) ≠ 1) : ∃ a, a ∈ s ∧ f a ≠ 1

ink

theorem Finset.sum_range_succ_comm {β : Type u} [inst : AddCommMonoid β] (f : ℕ → β) (n : ℕ) : (Finset.sum (Finset.range (n + 1)) fun x => f x) = f n + Finset.sum (Finset.range n) fun x => f x

ink

theorem Finset.prod_range_succ_comm {β : Type u} [inst : CommMonoid β] (f : ℕ → β) (n : ℕ) : (Finset.prod (Finset.range (n + 1)) fun x => f x) = f n * Finset.prod (Finset.range n) fun x => f x

ink

theorem Finset.sum_range_succ {β : Type u} [inst : AddCommMonoid β] (f : ℕ → β) (n : ℕ) : (Finset.sum (Finset.range (n + 1)) fun x => f x) = (Finset.sum (Finset.range n) fun x => f x) + f n

ink

theorem Finset.prod_range_succ {β : Type u} [inst : CommMonoid β] (f : ℕ → β) (n : ℕ) : (Finset.prod (Finset.range (n + 1)) fun x => f x) = (Finset.prod (Finset.range n) fun x => f x) * f n

ink

abbrev Finset.sum_range_succ'.match_1 (motive : ℕ → Prop) : (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive (Nat.succ n)) → motive x

Equations

• Finset.sum_range_succ'.match_1 motive x h_1 h_2 = Nat.casesOn x (h_1 ()) fun n => h_2 n

ink

theorem Finset.sum_range_succ' {β : Type u} [inst : AddCommMonoid β] (f : ℕ → β) (n : ℕ) : (Finset.sum (Finset.range (n + 1)) fun k => f k) = (Finset.sum (Finset.range n) fun k => f (k + 1)) + f 0

ink

theorem Finset.prod_range_succ' {β : Type u} [inst : CommMonoid β] (f : ℕ → β) (n : ℕ) : (Finset.prod (Finset.range (n + 1)) fun k => f k) = (Finset.prod (Finset.range n) fun k => f (k + 1)) * f 0

ink

theorem Finset.eventually_constant_sum {β : Type u} [inst : AddCommMonoid β] {u : ℕ → β} {N : ℕ} (hu : ∀ (n : ℕ), n ≥ N → u n = 0) {n : ℕ} (hn : N ≤ n) : (Finset.sum (Finset.range (n + 1)) fun k => u k) = Finset.sum (Finset.range (N + 1)) fun k => u k

ink

theorem Finset.eventually_constant_prod {β : Type u} [inst : CommMonoid β] {u : ℕ → β} {N : ℕ} (hu : ∀ (n : ℕ), n ≥ N → u n = 1) {n : ℕ} (hn : N ≤ n) : (Finset.prod (Finset.range (n + 1)) fun k => u k) = Finset.prod (Finset.range (N + 1)) fun k => u k

ink

theorem Finset.sum_range_add {β : Type u} [inst : AddCommMonoid β] (f : ℕ → β) (n : ℕ) (m : ℕ) : (Finset.sum (Finset.range (n + m)) fun x => f x) = (Finset.sum (Finset.range n) fun x => f x) + Finset.sum (Finset.range m) fun x => f (n + x)

ink

theorem Finset.prod_range_add {β : Type u} [inst : CommMonoid β] (f : ℕ → β) (n : ℕ) (m : ℕ) : (Finset.prod (Finset.range (n + m)) fun x => f x) = (Finset.prod (Finset.range n) fun x => f x) * Finset.prod (Finset.range m) fun x => f (n + x)

ink

theorem Finset.sum_range_add_sub_sum_range {α : Type u_1} [inst : AddCommGroup α] (f : ℕ → α) (n : ℕ) (m : ℕ) : ((Finset.sum (Finset.range (n + m)) fun k => f k) - Finset.sum (Finset.range n) fun k => f k) = Finset.sum (Finset.range m) fun k => f (n + k)

ink

theorem Finset.prod_range_add_div_prod_range {α : Type u_1} [inst : CommGroup α] (f : ℕ → α) (n : ℕ) (m : ℕ) : ((Finset.prod (Finset.range (n + m)) fun k => f k) / Finset.prod (Finset.range n) fun k => f k) = Finset.prod (Finset.range m) fun k => f (n + k)

ink

theorem Finset.sum_range_zero {β : Type u} [inst : AddCommMonoid β] (f : ℕ → β) : (Finset.sum (Finset.range 0) fun k => f k) = 0

ink

theorem Finset.prod_range_zero {β : Type u} [inst : CommMonoid β] (f : ℕ → β) : (Finset.prod (Finset.range 0) fun k => f k) = 1

ink

theorem Finset.sum_range_one {β : Type u} [inst : AddCommMonoid β] (f : ℕ → β) : (Finset.sum (Finset.range 1) fun k => f k) = f 0

ink

theorem Finset.prod_range_one {β : Type u} [inst : CommMonoid β] (f : ℕ → β) : (Finset.prod (Finset.range 1) fun k => f k) = f 0

ink

theorem Finset.sum_list_map_count {α : Type v} [inst : DecidableEq α] (l : List α) {M : Type u_1} [inst : AddCommMonoid M] (f : α → M) : List.sum (List.map f l) = Finset.sum (List.toFinset l) fun m => List.count m l • f m

ink

theorem Finset.prod_list_map_count {α : Type v} [inst : DecidableEq α] (l : List α) {M : Type u_1} [inst : CommMonoid M] (f : α → M) : List.prod (List.map f l) = Finset.prod (List.toFinset l) fun m => f m ^ List.count m l

ink

theorem Finset.sum_list_count {α : Type v} [inst : DecidableEq α] [inst : AddCommMonoid α] (s : List α) : List.sum s = Finset.sum (List.toFinset s) fun m => List.count m s • m

ink

theorem Finset.prod_list_count {α : Type v} [inst : DecidableEq α] [inst : CommMonoid α] (s : List α) : List.prod s = Finset.prod (List.toFinset s) fun m => m ^ List.count m s

ink

theorem Finset.sum_list_count_of_subset {α : Type v} [inst : DecidableEq α] [inst : AddCommMonoid α] (m : List α) (s : Finset α) (hs : List.toFinset m ⊆ s) : List.sum m = Finset.sum s fun i => List.count i m • i

ink

theorem Finset.prod_list_count_of_subset {α : Type v} [inst : DecidableEq α] [inst : CommMonoid α] (m : List α) (s : Finset α) (hs : List.toFinset m ⊆ s) : List.prod m = Finset.prod s fun i => i ^ List.count i m

ink

theorem Finset.sum_filter_count_eq_countp {α : Type v} [inst : DecidableEq α] (p : α → Prop) [inst : DecidablePred p] (l : List α) : (Finset.sum (Finset.filter p (List.toFinset l)) fun x => List.count x l) = List.countp (fun b => decide (p b)) l

ink

theorem Finset.sum_multiset_map_count {α : Type v} [inst : DecidableEq α] (s : Multiset α) {M : Type u_1} [inst : AddCommMonoid M] (f : α → M) : Multiset.sum (Multiset.map f s) = Finset.sum (Multiset.toFinset s) fun m => Multiset.count m s • f m

ink

theorem Finset.prod_multiset_map_count {α : Type v} [inst : DecidableEq α] (s : Multiset α) {M : Type u_1} [inst : CommMonoid M] (f : α → M) : Multiset.prod (Multiset.map f s) = Finset.prod (Multiset.toFinset s) fun m => f m ^ Multiset.count m s

ink

theorem Finset.sum_multiset_count {α : Type v} [inst : DecidableEq α] [inst : AddCommMonoid α] (s : Multiset α) : Multiset.sum s = Finset.sum (Multiset.toFinset s) fun m => Multiset.count m s • m

ink

theorem Finset.prod_multiset_count {α : Type v} [inst : DecidableEq α] [inst : CommMonoid α] (s : Multiset α) : Multiset.prod s = Finset.prod (Multiset.toFinset s) fun m => m ^ Multiset.count m s

ink

theorem Finset.sum_multiset_count_of_subset {α : Type v} [inst : DecidableEq α] [inst : AddCommMonoid α] (m : Multiset α) (s : Finset α) (hs : Multiset.toFinset m ⊆ s) : Multiset.sum m = Finset.sum s fun i => Multiset.count i m • i

ink

theorem Finset.prod_multiset_count_of_subset {α : Type v} [inst : DecidableEq α] [inst : CommMonoid α] (m : Multiset α) (s : Finset α) (hs : Multiset.toFinset m ⊆ s) : Multiset.prod m = Finset.prod s fun i => i ^ Multiset.count i m

ink

theorem Finset.sum_mem_multiset {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] (m : Multiset α) (f : { x // x ∈ m } → β) (g : α → β) (hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x) : (Finset.sum Finset.univ fun x => f x) = Finset.sum (Multiset.toFinset m) fun x => g x

ink

theorem Finset.prod_mem_multiset {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] (m : Multiset α) (f : { x // x ∈ m } → β) (g : α → β) (hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x) : (Finset.prod Finset.univ fun x => f x) = Finset.prod (Multiset.toFinset m) fun x => g x

ink

theorem Finset.sum_induction {α : Type v} {s : Finset α} {M : Type u_1} [inst : AddCommMonoid M] (f : α → M) (p : M → Prop) (hom : (a b : M) → p a → p b → p (a + b)) (unit : p 0) (base : (x : α) → x ∈ s → p (f x)) : p (Finset.sum s fun x => f x)

To prove a property of a sum, it suffices to prove that the property is additive and holds on summands.

ink

theorem Finset.prod_induction {α : Type v} {s : Finset α} {M : Type u_1} [inst : CommMonoid M] (f : α → M) (p : M → Prop) (hom : (a b : M) → p a → p b → p (a * b)) (unit : p 1) (base : (x : α) → x ∈ s → p (f x)) : p (Finset.prod s fun x => f x)

To prove a property of a product, it suffices to prove that the property is multiplicative and holds on factors.

ink

theorem Finset.sum_induction_nonempty {α : Type v} {s : Finset α} {M : Type u_1} [inst : AddCommMonoid M] (f : α → M) (p : M → Prop) (hom : (a b : M) → p a → p b → p (a + b)) (nonempty : Finset.Nonempty s) (base : (x : α) → x ∈ s → p (f x)) : p (Finset.sum s fun x => f x)

To prove a property of a sum, it suffices to prove that the property is additive and holds on summands.

ink

theorem Finset.prod_induction_nonempty {α : Type v} {s : Finset α} {M : Type u_1} [inst : CommMonoid M] (f : α → M) (p : M → Prop) (hom : (a b : M) → p a → p b → p (a * b)) (nonempty : Finset.Nonempty s) (base : (x : α) → x ∈ s → p (f x)) : p (Finset.prod s fun x => f x)

To prove a property of a product, it suffices to prove that the property is multiplicative and holds on factors.

ink

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

ink

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

ink

theorem Finset.sum_range_sub {M : Type u_1} [inst : AddCommGroup M] (f : ℕ → M) (n : ℕ) : (Finset.sum (Finset.range n) fun i => 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.

ink

theorem Finset.prod_range_div {M : Type u_1} [inst : CommGroup M] (f : ℕ → M) (n : ℕ) : (Finset.prod (Finset.range n) fun i => 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.

ink

theorem Finset.sum_range_sub' {M : Type u_1} [inst : AddCommGroup M] (f : ℕ → M) (n : ℕ) : (Finset.sum (Finset.range n) fun i => f i - f (i + 1)) = f 0 - f n

ink

theorem Finset.prod_range_div' {M : Type u_1} [inst : CommGroup M] (f : ℕ → M) (n : ℕ) : (Finset.prod (Finset.range n) fun i => f i / f (i + 1)) = f 0 / f n

ink

theorem Finset.eq_sum_range_sub {M : Type u_1} [inst : AddCommGroup M] (f : ℕ → M) (n : ℕ) : f n = f 0 + Finset.sum (Finset.range n) fun i => f (i + 1) - f i

ink

theorem Finset.eq_prod_range_div {M : Type u_1} [inst : CommGroup M] (f : ℕ → M) (n : ℕ) : f n = f 0 * Finset.prod (Finset.range n) fun i => f (i + 1) / f i

ink

theorem Finset.eq_sum_range_sub' {M : Type u_1} [inst : AddCommGroup M] (f : ℕ → M) (n : ℕ) : f n = Finset.sum (Finset.range (n + 1)) fun i => if i = 0 then f 0 else f i - f (i - 1)

ink

theorem Finset.eq_prod_range_div' {M : Type u_1} [inst : CommGroup M] (f : ℕ → M) (n : ℕ) : f n = Finset.prod (Finset.range (n + 1)) fun i => if i = 0 then f 0 else f i / f (i - 1)

ink

theorem Finset.sum_range_tsub {α : Type v} [inst : CanonicallyOrderedAddMonoid α] [inst : Sub α] [inst : OrderedSub α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {f : ℕ → α} (h : Monotone f) (n : ℕ) : (Finset.sum (Finset.range n) fun i => 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.

ink

@[simp]

theorem Finset.sum_const {β : Type u} {α : Type v} {s : Finset α} [inst : AddCommMonoid β] (b : β) : (Finset.sum s fun _x => b) = Finset.card s • b

ink

@[simp]

theorem Finset.prod_const {β : Type u} {α : Type v} {s : Finset α} [inst : CommMonoid β] (b : β) : (Finset.prod s fun _x => b) = b ^ Finset.card s

ink

theorem Finset.sum_eq_card_nsmul {β : Type u} {α : Type v} {s : Finset α} {f : α → β} [inst : AddCommMonoid β] {b : β} (hf : ∀ (a : α), a ∈ s → f a = b) : (Finset.sum s fun a => f a) = Finset.card s • b

ink

theorem Finset.prod_eq_pow_card {β : Type u} {α : Type v} {s : Finset α} {f : α → β} [inst : CommMonoid β] {b : β} (hf : ∀ (a : α), a ∈ s → f a = b) : (Finset.prod s fun a => f a) = b ^ Finset.card s

ink

theorem Finset.nsmul_eq_sum_const {β : Type u} [inst : AddCommMonoid β] (b : β) (n : ℕ) : n • b = Finset.sum (Finset.range n) fun _k => b

ink

theorem Finset.pow_eq_prod_const {β : Type u} [inst : CommMonoid β] (b : β) (n : ℕ) : b ^ n = Finset.prod (Finset.range n) fun _k => b

ink

theorem Finset.sum_nsmul {β : Type u} {α : Type v} [inst : AddCommMonoid β] (s : Finset α) (n : ℕ) (f : α → β) : (Finset.sum s fun x => n • f x) = n • Finset.sum s fun x => f x

ink

theorem Finset.prod_pow {β : Type u} {α : Type v} [inst : CommMonoid β] (s : Finset α) (n : ℕ) (f : α → β) : (Finset.prod s fun x => f x ^ n) = (Finset.prod s fun x => f x) ^ n

ink

theorem Finset.sum_flip {β : Type u} [inst : AddCommMonoid β] {n : ℕ} (f : ℕ → β) : (Finset.sum (Finset.range (n + 1)) fun r => f (n - r)) = Finset.sum (Finset.range (n + 1)) fun k => f k

ink

theorem Finset.prod_flip {β : Type u} [inst : CommMonoid β] {n : ℕ} (f : ℕ → β) : (Finset.prod (Finset.range (n + 1)) fun r => f (n - r)) = Finset.prod (Finset.range (n + 1)) fun k => f k

ink

theorem Finset.sum_involution {β : Type u} {α : Type v} [inst : AddCommMonoid β] {s : Finset α} {f : α → β} (g : (a : α) → a ∈ s → α) : (∀ (a : α) (ha : a ∈ s), f a + f (g a ha) = 0) → (∀ (a : α) (ha : a ∈ s), f a ≠ 0 → g a ha ≠ a) → ∀ (g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s), (∀ (a : α) (ha : a ∈ s), g (g a ha) (_ : g a ha ∈ s) = a) → (Finset.sum s fun x => f x) = 0

ink

abbrev Finset.sum_involution.match_1 {α : Type u_1} (s : Finset α) (motive : Finset.Nonempty s → Prop) : (x : Finset.Nonempty s) → ((x : α) → (hx : x ∈ s) → motive (_ : ∃ x, x ∈ s)) → motive x

Equations

• Finset.sum_involution.match_1 s motive x h_1 = Exists.casesOn x fun w h => h_1 w h

ink

theorem Finset.prod_involution {β : Type u} {α : Type v} [inst : CommMonoid β] {s : Finset α} {f : α → β} (g : (a : α) → a ∈ s → α) : (∀ (a : α) (ha : a ∈ s), f a * f (g a ha) = 1) → (∀ (a : α) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a) → ∀ (g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s), (∀ (a : α) (ha : a ∈ s), g (g a ha) (_ : g a ha ∈ s) = a) → (Finset.prod s fun x => f x) = 1

ink

theorem Finset.sum_comp {β : Type u} {α : Type v} {γ : Type w} {s : Finset α} [inst : AddCommMonoid β] [inst : DecidableEq γ] (f : γ → β) (g : α → γ) : (Finset.sum s fun a => f (g a)) = Finset.sum (Finset.image g s) fun b => Finset.card (Finset.filter (fun a => g a = b) s) • 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.

ink

theorem Finset.prod_comp {β : Type u} {α : Type v} {γ : Type w} {s : Finset α} [inst : CommMonoid β] [inst : DecidableEq γ] (f : γ → β) (g : α → γ) : (Finset.prod s fun a => f (g a)) = Finset.prod (Finset.image g s) fun b => f b ^ Finset.card (Finset.filter (fun a => g a = b) s)

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.

ink

theorem Finset.sum_piecewise {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (t : Finset α) (f : α → β) (g : α → β) : (Finset.sum s fun x => Finset.piecewise t f g x) = (Finset.sum (s ∩ t) fun x => f x) + Finset.sum (s \ t) fun x => g x

ink

theorem Finset.prod_piecewise {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (t : Finset α) (f : α → β) (g : α → β) : (Finset.prod s fun x => Finset.piecewise t f g x) = (Finset.prod (s ∩ t) fun x => f x) * Finset.prod (s \ t) fun x => g x

ink

theorem Finset.sum_inter_add_sum_diff {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (t : Finset α) (f : α → β) : ((Finset.sum (s ∩ t) fun x => f x) + Finset.sum (s \ t) fun x => f x) = Finset.sum s fun x => f x

ink

theorem Finset.prod_inter_mul_prod_diff {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (t : Finset α) (f : α → β) : ((Finset.prod (s ∩ t) fun x => f x) * Finset.prod (s \ t) fun x => f x) = Finset.prod s fun x => f x

ink

theorem Finset.sum_eq_add_sum_diff_singleton {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) : (Finset.sum s fun x => f x) = f i + Finset.sum (s \ {i}) fun x => f x

ink

theorem Finset.prod_eq_mul_prod_diff_singleton {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) : (Finset.prod s fun x => f x) = f i * Finset.prod (s \ {i}) fun x => f x

ink

theorem Finset.sum_eq_sum_diff_singleton_add {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) : (Finset.sum s fun x => f x) = (Finset.sum (s \ {i}) fun x => f x) + f i

ink

theorem Finset.prod_eq_prod_diff_singleton_mul {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) : (Finset.prod s fun x => f x) = (Finset.prod (s \ {i}) fun x => f x) * f i

ink

theorem Fintype.sum_eq_add_sum_compl {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] [inst : Fintype α] (a : α) (f : α → β) : (Finset.sum Finset.univ fun i => f i) = f a + Finset.sum ({a}ᶜ) fun i => f i

ink

theorem Fintype.prod_eq_mul_prod_compl {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] [inst : Fintype α] (a : α) (f : α → β) : (Finset.prod Finset.univ fun i => f i) = f a * Finset.prod ({a}ᶜ) fun i => f i

ink

theorem Fintype.sum_eq_sum_compl_add {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] [inst : Fintype α] (a : α) (f : α → β) : (Finset.sum Finset.univ fun i => f i) = (Finset.sum ({a}ᶜ) fun i => f i) + f a

ink

theorem Fintype.prod_eq_prod_compl_mul {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] [inst : Fintype α] (a : α) (f : α → β) : (Finset.prod Finset.univ fun i => f i) = (Finset.prod ({a}ᶜ) fun i => f i) * f a

ink

theorem Finset.dvd_prod_of_mem {β : Type u} {α : Type v} [inst : CommMonoid β] (f : α → β) {a : α} {s : Finset α} (ha : a ∈ s) : f a ∣ Finset.prod s fun i => f i

ink

theorem Finset.sum_partition {β : Type u} {α : Type v} {s : Finset α} {f : α → β} [inst : AddCommMonoid β] (R : Setoid α) [inst : DecidableRel Setoid.r] : (Finset.sum s fun x => f x) = Finset.sum (Finset.image Quotient.mk'' s) fun xbar => Finset.sum (Finset.filter (fun x => Quotient.mk R x = xbar) s) fun y => f y

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

ink

theorem Finset.prod_partition {β : Type u} {α : Type v} {s : Finset α} {f : α → β} [inst : CommMonoid β] (R : Setoid α) [inst : DecidableRel Setoid.r] : (Finset.prod s fun x => f x) = Finset.prod (Finset.image Quotient.mk'' s) fun xbar => Finset.prod (Finset.filter (fun x => Quotient.mk R x = xbar) s) fun y => f y

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

ink

theorem Finset.sum_cancels_of_partition_cancels {β : Type u} {α : Type v} {s : Finset α} {f : α → β} [inst : AddCommMonoid β] (R : Setoid α) [inst : DecidableRel Setoid.r] (h : ∀ (x : α), x ∈ s → (Finset.sum (Finset.filter (fun y => y ≈ x) s) fun a => f a) = 0) : (Finset.sum s fun x => f x) = 0

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

ink

theorem Finset.prod_cancels_of_partition_cancels {β : Type u} {α : Type v} {s : Finset α} {f : α → β} [inst : CommMonoid β] (R : Setoid α) [inst : DecidableRel Setoid.r] (h : ∀ (x : α), x ∈ s → (Finset.prod (Finset.filter (fun y => y ≈ x) s) fun a => f a) = 1) : (Finset.prod s fun x => f x) = 1

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

ink

theorem Finset.sum_update_of_not_mem {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] {s : Finset α} {i : α} (h : ¬i ∈ s) (f : α → β) (b : β) : (Finset.sum s fun x => Function.update f i b x) = Finset.sum s fun x => f x

ink

theorem Finset.prod_update_of_not_mem {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] {s : Finset α} {i : α} (h : ¬i ∈ s) (f : α → β) (b : β) : (Finset.prod s fun x => Function.update f i b x) = Finset.prod s fun x => f x

ink

theorem Finset.sum_update_of_mem {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) (b : β) : (Finset.sum s fun x => Function.update f i b x) = b + Finset.sum (s \ {i}) fun x => f x

ink

theorem Finset.prod_update_of_mem {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] {s : Finset α} {i : α} (h : i ∈ s) (f : α → β) (b : β) : (Finset.prod s fun x => Function.update f i b x) = b * Finset.prod (s \ {i}) fun x => f x

ink

theorem Finset.eq_of_card_le_one_of_sum_eq {β : Type u} {α : Type v} [inst : AddCommMonoid β] {s : Finset α} (hc : Finset.card s ≤ 1) {f : α → β} {b : β} (h : (Finset.sum s fun x => 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.

ink

theorem Finset.eq_of_card_le_one_of_prod_eq {β : Type u} {α : Type v} [inst : CommMonoid β] {s : Finset α} (hc : Finset.card s ≤ 1) {f : α → β} {b : β} (h : (Finset.prod s fun x => 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.

ink

theorem Finset.add_sum_erase {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (f : α → β) {a : α} (h : a ∈ s) : (f a + Finset.sum (Finset.erase s a) fun x => f x) = Finset.sum s fun x => 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.

ink

theorem Finset.mul_prod_erase {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (f : α → β) {a : α} (h : a ∈ s) : (f a * Finset.prod (Finset.erase s a) fun x => f x) = Finset.prod s fun x => 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.

ink

theorem Finset.sum_erase_add {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) (f : α → β) {a : α} (h : a ∈ s) : (Finset.sum (Finset.erase s a) fun x => f x) + f a = Finset.sum s fun x => f x

A variant of Finset.add_sum_erase with the addition swapped.

ink

theorem Finset.prod_erase_mul {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] (s : Finset α) (f : α → β) {a : α} (h : a ∈ s) : (Finset.prod (Finset.erase s a) fun x => f x) * f a = Finset.prod s fun x => f x

A variant of Finset.mul_prod_erase with the multiplication swapped.

ink

theorem Finset.sum_erase {β : Type u} {α : Type v} [inst : AddCommMonoid β] [inst : DecidableEq α] (s : Finset α) {f : α → β} {a : α} (h : f a = 0) : (Finset.sum (Finset.erase s a) fun x => f x) = Finset.sum s fun x => f x

If a function applied at a point is 0, a sum is unchanged by removing that point, if present, from a Finset.

ink

theorem Finset.prod_erase {β : Type u} {α : Type v} [inst : CommMonoid β] [inst : DecidableEq α] (s : Finset α) {f : α → β} {a : α} (h : f a = 1) : (Finset.prod (Finset.erase s a) fun x => f x) = Finset.prod s fun x => f x

If a function applied at a point is 1, a product is unchanged by removing that point, if present, from a Finset.

ink

theorem Finset.sum_ite_zero {β : Type u} {α : Type v} {s : Finset α} [inst : AddCommMonoid β] {f : α → Prop} [inst : DecidablePred f] (hf : Set.PairwiseDisjoint (↑s) f) (a : β) : (Finset.sum s fun i => if f i then a else 0) = if ∃ i, i ∈ s ∧ f i then a else 0

See also Finset.sum_boole.

ink

theorem Finset.prod_ite_one {β : Type u} {α : Type v} {s : Finset α} [inst : CommMonoid β] {f : α → Prop} [inst : DecidablePred f] (hf : Set.PairwiseDisjoint (↑s) f) (a : β) : (Finset.prod s fun i => if f i then a else 1) = if ∃ i, i ∈ s ∧ f i then a else 1

See also Finset.prod_boole.

ink

theorem Finset.