Big operators #
In this file we define products and sums indexed by finite sets (specifically, finset).
Notation #
We introduce the following notation, localized in big_operators.
To enable the notation, use open_locale big_operators.
Let s be a finset α, and f : α → β a function.
∏ x in s, f xis notation forfinset.prod s f(assumingβis acomm_monoid)∑ x in s, f xis notation forfinset.sum s f(assumingβis anadd_comm_monoid)∏ x, f xis notation forfinset.prod finset.univ f(assumingαis afintypeandβis acomm_monoid)∑ x, f xis notation forfinset.sum finset.univ f(assumingαis afintypeandβis anadd_comm_monoid)
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.
@[protected]
∑ x in s, f x is the sum of f x as x ranges over the elements
of the finite set s.
Equations
- s.sum f = (multiset.map f s.val).sum
@[protected]
∏ x in s, f x is the product of f x
as x ranges over the elements of the finite set s.
Equations
- s.prod f = (multiset.map f s.val).prod
@[simp]
theorem
finset.prod_mk
{β : Type u}
{α : Type v}
[comm_monoid β]
(s : multiset α)
(hs : s.nodup)
(f : α → β) :
@[simp]
theorem
finset.sum_mk
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(s : multiset α)
(hs : s.nodup)
(f : α → β) :
theorem
finset.prod_eq_multiset_prod
{β : Type u}
{α : Type v}
[comm_monoid β]
(s : finset α)
(f : α → β) :
∏ (x : α) in s, f x = (multiset.map f s.val).prod
theorem
finset.sum_eq_multiset_sum
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(s : finset α)
(f : α → β) :
∑ (x : α) in s, f x = (multiset.map f s.val).sum
theorem
finset.prod_eq_fold
{β : Type u}
{α : Type v}
[comm_monoid β]
(s : finset α)
(f : α → β) :
∏ (x : α) in s, f x = finset.fold has_mul.mul 1 f s
theorem
finset.sum_eq_fold
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(s : finset α)
(f : α → β) :
∑ (x : α) in s, f x = finset.fold has_add.add 0 f s
@[simp]
theorem
map_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
[add_comm_monoid γ]
{G : Type u_1}
[add_monoid_hom_class G β γ]
(g : G)
(f : α → β)
(s : finset α) :
theorem
map_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
[comm_monoid γ]
{G : Type u_1}
[monoid_hom_class G β γ]
(g : G)
(f : α → β)
(s : finset α) :
@[protected]
theorem
add_monoid_hom.map_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
[add_comm_monoid γ]
(g : β →+ γ)
(f : α → β)
(s : finset α) :
Deprecated: use _root_.map_sum instead.
@[protected]
theorem
monoid_hom.map_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
[comm_monoid γ]
(g : β →* γ)
(f : α → β)
(s : finset α) :
Deprecated: use _root_.map_prod instead.
@[protected]
theorem
add_equiv.map_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
[add_comm_monoid γ]
(g : β ≃+ γ)
(f : α → β)
(s : finset α) :
Deprecated: use _root_.map_sum instead.
@[protected]
theorem
mul_equiv.map_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
[comm_monoid γ]
(g : β ≃* γ)
(f : α → β)
(s : finset α) :
Deprecated: use _root_.map_prod instead.
@[protected]
theorem
ring_hom.map_list_sum
{β : Type u}
{γ : Type w}
[non_assoc_semiring β]
[non_assoc_semiring γ]
(f : β →+* γ)
(l : list β) :
Deprecated: use _root_.map_list_sum instead.
@[protected]
theorem
ring_hom.unop_map_list_prod
{β : Type u}
{γ : Type w}
[semiring β]
[semiring γ]
(f : β →+* γᵐᵒᵖ)
(l : list β) :
mul_opposite.unop (⇑f l.prod) = (list.map (mul_opposite.unop ∘ ⇑f) l).reverse.prod
A morphism into the opposite ring acts on the product by acting on the reversed elements.
Deprecated: use _root_.unop_map_list_prod instead.
@[protected]
theorem
ring_hom.map_multiset_prod
{β : Type u}
{γ : Type w}
[comm_semiring β]
[comm_semiring γ]
(f : β →+* γ)
(s : multiset β) :
Deprecated: use _root_.map_multiset_prod instead.
@[protected]
theorem
ring_hom.map_multiset_sum
{β : Type u}
{γ : Type w}
[non_assoc_semiring β]
[non_assoc_semiring γ]
(f : β →+* γ)
(s : multiset β) :
Deprecated: use _root_.map_multiset_sum instead.
@[protected]
theorem
ring_hom.map_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_semiring β]
[comm_semiring γ]
(g : β →+* γ)
(f : α → β)
(s : finset α) :
Deprecated: use _root_.map_prod instead.
@[protected]
theorem
ring_hom.map_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[non_assoc_semiring β]
[non_assoc_semiring γ]
(g : β →+* γ)
(f : α → β)
(s : finset α) :
Deprecated: use _root_.map_sum instead.
theorem
add_monoid_hom.coe_finset_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[add_zero_class β]
[add_comm_monoid γ]
(f : α → β →+ γ)
(s : finset α) :
theorem
monoid_hom.coe_finset_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[mul_one_class β]
[comm_monoid γ]
(f : α → β →* γ)
(s : finset α) :
@[simp]
theorem
add_monoid_hom.finset_sum_apply
{β : Type u}
{α : Type v}
{γ : Type w}
[add_zero_class β]
[add_comm_monoid γ]
(f : α → β →+ γ)
(s : finset α)
(b : β) :
@[simp]
theorem
monoid_hom.finset_prod_apply
{β : Type u}
{α : Type v}
{γ : Type w}
[mul_one_class β]
[comm_monoid γ]
(f : α → β →* γ)
(s : finset α)
(b : β) :
@[simp]
@[simp]
@[simp]
theorem
finset.sum_cons
{β : Type u}
{α : Type v}
{s : finset α}
{a : α}
{f : α → β}
[add_comm_monoid β]
(h : a ∉ s) :
∑ (x : α) in finset.cons a s h, f x = f a + ∑ (x : α) in s, f x
@[simp]
theorem
finset.prod_cons
{β : Type u}
{α : Type v}
{s : finset α}
{a : α}
{f : α → β}
[comm_monoid β]
(h : a ∉ s) :
∏ (x : α) in finset.cons a s h, f x = (f a) * ∏ (x : α) in s, f x
@[simp]
theorem
finset.prod_insert
{β : Type u}
{α : Type v}
{s : finset α}
{a : α}
{f : α → β}
[comm_monoid β]
[decidable_eq α] :
@[simp]
theorem
finset.sum_insert
{β : Type u}
{α : Type v}
{s : finset α}
{a : α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α] :
@[simp]
theorem
finset.sum_insert_of_eq_zero_if_not_mem
{β : Type u}
{α : Type v}
{s : finset α}
{a : α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
(h : a ∉ s → f a = 0) :
The sum of f over insert a s is the same as
the sum over s, as long as a is in s or f a = 0.
@[simp]
theorem
finset.prod_insert_of_eq_one_if_not_mem
{β : Type u}
{α : Type v}
{s : finset α}
{a : α}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
(h : a ∉ s → f a = 1) :
The product of f over insert a s is the same as
the product over s, as long as a is in s or f a = 1.
@[simp]
theorem
finset.sum_insert_zero
{β : Type u}
{α : Type v}
{s : finset α}
{a : α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
(h : f a = 0) :
The sum of f over insert a s is the same as
the sum over s, as long as f a = 0.
@[simp]
theorem
finset.prod_insert_one
{β : Type u}
{α : Type v}
{s : finset α}
{a : α}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
(h : f a = 1) :
The product of f over insert a s is the same as the product over s, as long as f a = 1.
@[simp]
theorem
finset.prod_singleton
{β : Type u}
{α : Type v}
{a : α}
{f : α → β}
[comm_monoid β] :
∏ (x : α) in {a}, f x = f a
@[simp]
theorem
finset.sum_singleton
{β : Type u}
{α : Type v}
{a : α}
{f : α → β}
[add_comm_monoid β] :
∑ (x : α) in {a}, f x = f a
theorem
finset.prod_pair
{β : Type u}
{α : Type v}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
{a b : α}
(h : a ≠ b) :
theorem
finset.sum_pair
{β : Type u}
{α : Type v}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
{a b : α}
(h : a ≠ b) :
@[simp]
theorem
finset.prod_const_one
{β : Type u}
{α : Type v}
{s : finset α}
[comm_monoid β] :
∏ (x : α) in s, 1 = 1
@[simp]
theorem
finset.sum_const_zero
{β : Type u}
{α : Type v}
{s : finset α}
[add_comm_monoid β] :
∑ (x : α) in s, 0 = 0
@[simp]
theorem
finset.sum_image
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
{s : finset γ}
{g : γ → α} :
@[simp]
theorem
finset.prod_image
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
{s : finset γ}
{g : γ → α} :
@[simp]
theorem
finset.sum_map
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
(s : finset α)
(e : α ↪ γ)
(f : γ → β) :
∑ (x : γ) in finset.map e s, f x = ∑ (x : α) in s, f (⇑e x)
@[simp]
theorem
finset.prod_map
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
(s : finset α)
(e : α ↪ γ)
(f : γ → β) :
∏ (x : γ) in finset.map e s, f x = ∏ (x : α) in s, f (⇑e x)
theorem
finset.prod_congr
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f g : α → β}
[comm_monoid β]
(h : s₁ = s₂) :
theorem
finset.sum_congr
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f g : α → β}
[add_comm_monoid β]
(h : s₁ = s₂) :
theorem
finset.sum_union_inter
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α] :
theorem
finset.prod_union_inter
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[comm_monoid β]
[decidable_eq α] :
theorem
finset.prod_union
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
(h : disjoint s₁ s₂) :
theorem
finset.sum_union
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
(h : disjoint s₁ s₂) :
theorem
finset.sum_filter_add_sum_filter_not
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(s : finset α)
(p : α → Prop)
[decidable_pred p]
[decidable_pred (λ (x : α), ¬p x)]
(f : α → β) :
∑ (x : α) in finset.filter p s, f x + ∑ (x : α) in finset.filter (λ (x : α), ¬p x) s, f x = ∑ (x : α) in s, f x
theorem
finset.prod_filter_mul_prod_filter_not
{β : Type u}
{α : Type v}
[comm_monoid β]
(s : finset α)
(p : α → Prop)
[decidable_pred p]
[decidable_pred (λ (x : α), ¬p x)]
(f : α → β) :
(∏ (x : α) in finset.filter p s, f x) * ∏ (x : α) in finset.filter (λ (x : α), ¬p x) s, f x = ∏ (x : α) in s, f x
@[simp]
@[simp]
theorem
finset.sum_to_list
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(s : finset α)
(f : α → β) :
theorem
equiv.perm.sum_comp
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(σ : equiv.perm α)
(s : finset α)
(f : α → β)
(hs : {a : α | ⇑σ a ≠ a} ⊆ ↑s) :
theorem
equiv.perm.prod_comp
{β : Type u}
{α : Type v}
[comm_monoid β]
(σ : equiv.perm α)
(s : finset α)
(f : α → β)
(hs : {a : α | ⇑σ a ≠ a} ⊆ ↑s) :
theorem
equiv.perm.sum_comp'
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(σ : equiv.perm α)
(s : finset α)
(f : α → α → β)
(hs : {a : α | ⇑σ a ≠ a} ⊆ ↑s) :
∑ (x : α) in s, f (⇑σ x) x = ∑ (x : α) in s, f x (⇑(equiv.symm σ) x)
theorem
equiv.perm.prod_comp'
{β : Type u}
{α : Type v}
[comm_monoid β]
(σ : equiv.perm α)
(s : finset α)
(f : α → α → β)
(hs : {a : α | ⇑σ a ≠ a} ⊆ ↑s) :
∏ (x : α) in s, f (⇑σ x) x = ∏ (x : α) in s, f x (⇑(equiv.symm σ) x)
theorem
is_compl.sum_add_sum
{β : Type u}
{α : Type v}
[fintype α]
[decidable_eq α]
[add_comm_monoid β]
{s t : finset α}
(h : is_compl s t)
(f : α → β) :
theorem
is_compl.prod_mul_prod
{β : Type u}
{α : Type v}
[fintype α]
[decidable_eq α]
[comm_monoid β]
{s t : finset α}
(h : is_compl s t)
(f : α → β) :
theorem
finset.sum_add_sum_compl
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[fintype α]
[decidable_eq α]
(s : finset α)
(f : α → β) :
Adding the sums of a function over s and over sᶜ gives the whole sum.
For a version expressed with subtypes, see fintype.sum_subtype_add_sum_subtype.
theorem
finset.prod_mul_prod_compl
{β : Type u}
{α : Type v}
[comm_monoid β]
[fintype α]
[decidable_eq α]
(s : finset α)
(f : α → β) :
Multiplying the products of a function over s and over sᶜ gives the whole product.
For a version expressed with subtypes, see fintype.prod_subtype_mul_prod_subtype.
theorem
finset.prod_compl_mul_prod
{β : Type u}
{α : Type v}
[comm_monoid β]
[fintype α]
[decidable_eq α]
(s : finset α)
(f : α → β) :
theorem
finset.sum_compl_add_sum
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[fintype α]
[decidable_eq α]
(s : finset α)
(f : α → β) :
theorem
finset.prod_sdiff
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
(h : s₁ ⊆ s₂) :
theorem
finset.sum_sdiff
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
(h : s₁ ⊆ s₂) :
@[simp]
theorem
finset.sum_sum_elim
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
[decidable_eq (α ⊕ γ)]
(s : finset α)
(t : finset γ)
(f : α → β)
(g : γ → β) :
∑ (x : α ⊕ γ) in finset.map function.embedding.inl s ∪ finset.map function.embedding.inr t, sum.elim f g x = ∑ (x : α) in s, f x + ∑ (x : γ) in t, g x
@[simp]
theorem
finset.prod_sum_elim
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
[decidable_eq (α ⊕ γ)]
(s : finset α)
(t : finset γ)
(f : α → β)
(g : γ → β) :
∏ (x : α ⊕ γ) in finset.map function.embedding.inl s ∪ finset.map function.embedding.inr t, sum.elim f g x = (∏ (x : α) in s, f x) * ∏ (x : γ) in t, g x
theorem
finset.prod_bUnion
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
{s : finset γ}
{t : γ → finset α}
(hs : ↑s.pairwise_disjoint t) :
theorem
finset.sum_bUnion
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
{s : finset γ}
{t : γ → finset α}
(hs : ↑s.pairwise_disjoint t) :
theorem
finset.prod_sigma
{β : Type u}
{α : Type v}
[comm_monoid β]
{σ : α → Type u_1}
(s : finset α)
(t : Π (a : α), finset (σ a))
(f : sigma σ → β) :
Product over a sigma type equals the product of fiberwise products. For rewriting
in the reverse direction, use finset.prod_sigma'.
theorem
finset.sum_sigma
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{σ : α → Type u_1}
(s : finset α)
(t : Π (a : α), finset (σ a))
(f : sigma σ → β) :
Sum over a sigma type equals the sum of fiberwise sums. For rewriting
in the reverse direction, use finset.sum_sigma'
theorem
finset.sum_sigma'
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{σ : α → Type u_1}
(s : finset α)
(t : Π (a : α), finset (σ a))
(f : Π (a : α), σ a → β) :
theorem
finset.prod_sigma'
{β : Type u}
{α : Type v}
[comm_monoid β]
{σ : α → Type u_1}
(s : finset α)
(t : Π (a : α), finset (σ a))
(f : Π (a : α), σ a → β) :
theorem
finset.sum_bij
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{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 : a ∈ s), b = i a ha)) :
∑ (x : α) in s, f x = ∑ (x : γ) in t, 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.
theorem
finset.prod_bij
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
{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 : a ∈ s), b = i a ha)) :
∏ (x : α) in s, f x = ∏ (x : γ) in t, 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.
theorem
finset.sum_bij'
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{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) _ = a)
(right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) _ = a) :
∑ (x : α) in s, f x = ∑ (x : γ) in t, 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.
theorem
finset.prod_bij'
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
{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) _ = a)
(right_inv : ∀ (a : γ) (ha : a ∈ t), i (j a ha) _ = a) :
∏ (x : α) in s, f x = ∏ (x : γ) in t, 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.
theorem
finset.prod_fiberwise_of_maps_to
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
[decidable_eq γ]
{s : finset α}
{t : finset γ}
{g : α → γ}
(h : ∀ (x : α), x ∈ s → g x ∈ t)
(f : α → β) :
∏ (y : γ) in t, ∏ (x : α) in finset.filter (λ (x : α), g x = y) s, f x = ∏ (x : α) in s, f x
theorem
finset.sum_fiberwise_of_maps_to
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
[decidable_eq γ]
{s : finset α}
{t : finset γ}
{g : α → γ}
(h : ∀ (x : α), x ∈ s → g x ∈ t)
(f : α → β) :
∑ (y : γ) in t, ∑ (x : α) in finset.filter (λ (x : α), g x = y) s, f x = ∑ (x : α) in s, f x
theorem
finset.prod_image'
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[comm_monoid β]
[decidable_eq α]
{s : finset γ}
{g : γ → α}
(h : γ → β)
(eq : ∀ (c : γ), c ∈ s → f (g c) = ∏ (x : γ) in finset.filter (λ (c' : γ), g c' = g c) s, h x) :
∏ (x : α) in finset.image g s, f x = ∏ (x : γ) in s, h x
theorem
finset.sum_image'
{β : Type u}
{α : Type v}
{γ : Type w}
{f : α → β}
[add_comm_monoid β]
[decidable_eq α]
{s : finset γ}
{g : γ → α}
(h : γ → β)
(eq : ∀ (c : γ), c ∈ s → f (g c) = ∑ (x : γ) in finset.filter (λ (c' : γ), g c' = g c) s, h x) :
∑ (x : α) in finset.image g s, f x = ∑ (x : γ) in s, h x
theorem
finset.prod_mul_distrib
{β : Type u}
{α : Type v}
{s : finset α}
{f g : α → β}
[comm_monoid β] :
theorem
finset.sum_add_distrib
{β : Type u}
{α : Type v}
{s : finset α}
{f g : α → β}
[add_comm_monoid β] :
theorem
finset.prod_comm
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
{s : finset γ}
{t : finset α}
{f : γ → α → β} :
∏ (x : γ) in s, ∏ (y : α) in t, f x y = ∏ (y : α) in t, ∏ (x : γ) in s, f x y
theorem
finset.sum_comm
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{s : finset γ}
{t : finset α}
{f : γ → α → β} :
∑ (x : γ) in s, ∑ (y : α) in t, f x y = ∑ (y : α) in t, ∑ (x : γ) in s, f x y
theorem
finset.prod_product
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
{s : finset γ}
{t : finset α}
{f : γ × α → β} :
theorem
finset.sum_product
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{s : finset γ}
{t : finset α}
{f : γ × α → β} :
theorem
finset.sum_product'
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{s : finset γ}
{t : finset α}
{f : γ → α → β} :
An uncurried version of finset.sum_product
theorem
finset.prod_product'
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
{s : finset γ}
{t : finset α}
{f : γ → α → β} :
An uncurried version of finset.prod_product.
theorem
finset.sum_product_right
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{s : finset γ}
{t : finset α}
{f : γ × α → β} :
theorem
finset.prod_product_right
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
{s : finset γ}
{t : finset α}
{f : γ × α → β} :
theorem
finset.prod_product_right'
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
{s : finset γ}
{t : finset α}
{f : γ → α → β} :
An uncurried version of finset.prod_product_right.
theorem
finset.sum_product_right'
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{s : finset γ}
{t : finset α}
{f : γ → α → β} :
An uncurried version of finset.prod_product_right
theorem
finset.sum_hom_rel
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
[add_comm_monoid γ]
{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 (∑ (x : α) in s, f x) (∑ (x : α) in s, g x)
theorem
finset.prod_hom_rel
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
[comm_monoid γ]
{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 (∏ (x : α) in s, f x) (∏ (x : α) in s, g x)
theorem
finset.sum_eq_zero
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{f : α → β}
{s : finset α}
(h : ∀ (x : α), x ∈ s → f x = 0) :
∑ (x : α) in s, f x = 0
theorem
finset.prod_eq_one
{β : Type u}
{α : Type v}
[comm_monoid β]
{f : α → β}
{s : finset α}
(h : ∀ (x : α), x ∈ s → f x = 1) :
∏ (x : α) in s, f x = 1
theorem
finset.sum_subset_zero_on_sdiff
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f g : α → β}
[add_comm_monoid β]
[decidable_eq α]
(h : s₁ ⊆ s₂)
(hg : ∀ (x : α), x ∈ s₂ \ s₁ → g x = 0)
(hfg : ∀ (x : α), x ∈ s₁ → f x = g x) :
∑ (i : α) in s₁, f i = ∑ (i : α) in s₂, g i
theorem
finset.prod_subset_one_on_sdiff
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f g : α → β}
[comm_monoid β]
[decidable_eq α]
(h : s₁ ⊆ s₂)
(hg : ∀ (x : α), x ∈ s₂ \ s₁ → g x = 1)
(hfg : ∀ (x : α), x ∈ s₁ → f x = g x) :
∏ (i : α) in s₁, f i = ∏ (i : α) in s₂, g i
theorem
finset.sum_subset
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[add_comm_monoid β]
(h : s₁ ⊆ s₂)
(hf : ∀ (x : α), x ∈ s₂ → x ∉ s₁ → f x = 0) :
∑ (x : α) in s₁, f x = ∑ (x : α) in s₂, f x
theorem
finset.prod_subset
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[comm_monoid β]
(h : s₁ ⊆ s₂)
(hf : ∀ (x : α), x ∈ s₂ → x ∉ s₁ → f x = 1) :
∏ (x : α) in s₁, f x = ∏ (x : α) in s₂, f x
theorem
finset.prod_filter_of_ne
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[comm_monoid β]
{p : α → Prop}
[decidable_pred p]
(hp : ∀ (x : α), x ∈ s → f x ≠ 1 → p x) :
∏ (x : α) in finset.filter p s, f x = ∏ (x : α) in s, f x
theorem
finset.sum_filter_of_ne
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[add_comm_monoid β]
{p : α → Prop}
[decidable_pred p]
(hp : ∀ (x : α), x ∈ s → f x ≠ 0 → p x) :
∑ (x : α) in finset.filter p s, f x = ∑ (x : α) in s, f x
theorem
finset.prod_filter_ne_one
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[comm_monoid β]
[Π (x : α), decidable (f x ≠ 1)] :
∏ (x : α) in finset.filter (λ (x : α), f x ≠ 1) s, f x = ∏ (x : α) in s, f x
theorem
finset.sum_filter_ne_zero
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[add_comm_monoid β]
[Π (x : α), decidable (f x ≠ 0)] :
∑ (x : α) in finset.filter (λ (x : α), f x ≠ 0) s, f x = ∑ (x : α) in s, f x
theorem
finset.prod_filter
{β : Type u}
{α : Type v}
{s : finset α}
[comm_monoid β]
(p : α → Prop)
[decidable_pred p]
(f : α → β) :
∏ (a : α) in finset.filter p s, f a = ∏ (a : α) in s, ite (p a) (f a) 1
theorem
finset.sum_filter
{β : Type u}
{α : Type v}
{s : finset α}
[add_comm_monoid β]
(p : α → Prop)
[decidable_pred p]
(f : α → β) :
∑ (a : α) in finset.filter p s, f a = ∑ (a : α) in s, ite (p a) (f a) 0
theorem
finset.prod_eq_single_of_mem
{β : Type u}
{α : Type v}
[comm_monoid β]
{s : finset α}
{f : α → β}
(a : α)
(h : a ∈ s)
(h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 1) :
∏ (x : α) in s, f x = f a
theorem
finset.sum_eq_single_of_mem
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{s : finset α}
{f : α → β}
(a : α)
(h : a ∈ s)
(h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 0) :
∑ (x : α) in s, f x = f a
theorem
finset.sum_eq_single
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{s : finset α}
{f : α → β}
(a : α)
(h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 0)
(h₁ : a ∉ s → f a = 0) :
∑ (x : α) in s, f x = f a
theorem
finset.prod_eq_single
{β : Type u}
{α : Type v}
[comm_monoid β]
{s : finset α}
{f : α → β}
(a : α)
(h₀ : ∀ (b : α), b ∈ s → b ≠ a → f b = 1)
(h₁ : a ∉ s → f a = 1) :
∏ (x : α) in s, f x = f a
theorem
finset.sum_attach
{β : Type u}
{α : Type v}
{s : finset α}
[add_comm_monoid β]
{f : α → β} :
@[simp]
theorem
finset.prod_subtype_eq_prod_filter
{β : Type u}
{α : Type v}
{s : finset α}
[comm_monoid β]
(f : α → β)
{p : α → Prop}
[decidable_pred p] :
∏ (x : subtype p) in finset.subtype p s, f ↑x = ∏ (x : α) in finset.filter p s, f x
A product over s.subtype p equals one over s.filter p.
@[simp]
theorem
finset.sum_subtype_eq_sum_filter
{β : Type u}
{α : Type v}
{s : finset α}
[add_comm_monoid β]
(f : α → β)
{p : α → Prop}
[decidable_pred p] :
∑ (x : subtype p) in finset.subtype p s, f ↑x = ∑ (x : α) in finset.filter p s, f x
A sum over s.subtype p equals one over s.filter p.
theorem
finset.prod_subtype_of_mem
{β : Type u}
{α : Type v}
{s : finset α}
[comm_monoid β]
(f : α → β)
{p : α → Prop}
[decidable_pred p]
(h : ∀ (x : α), x ∈ s → p x) :
∏ (x : subtype p) in finset.subtype p s, f ↑x = ∏ (x : α) in s, f x
If all elements of a finset satisfy the predicate p, a product
over s.subtype p equals that product over s.
theorem
finset.sum_subtype_of_mem
{β : Type u}
{α : Type v}
{s : finset α}
[add_comm_monoid β]
(f : α → β)
{p : α → Prop}
[decidable_pred p]
(h : ∀ (x : α), x ∈ s → p x) :
∑ (x : subtype p) in finset.subtype p s, f ↑x = ∑ (x : α) in s, f x
If all elements of a finset satisfy the predicate p, a sum
over s.subtype p equals that sum over s.
theorem
finset.sum_subtype_map_embedding
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{p : α → Prop}
{s : finset {x // p x}}
{f : {x // p x} → β}
{g : α → β}
(h : ∀ (x : {x // p x}), x ∈ s → g ↑x = f x) :
∑ (x : α) in finset.map (function.embedding.subtype (λ (x : α), p x)) s, g x = ∑ (x : {x // p x}) in s, f x
A sum of a function over a finset in a subtype equals a
sum in the main type of a function that agrees with the first
function on that finset.
theorem
finset.prod_subtype_map_embedding
{β : Type u}
{α : Type v}
[comm_monoid β]
{p : α → Prop}
{s : finset {x // p x}}
{f : {x // p x} → β}
{g : α → β}
(h : ∀ (x : {x // p x}), x ∈ s → g ↑x = f x) :
∏ (x : α) in finset.map (function.embedding.subtype (λ (x : α), p x)) s, g x = ∏ (x : {x // p x}) in s, f x
A product of a function over a finset in a subtype equals a
product in the main type of a function that agrees with the first
function on that finset.
theorem
finset.sum_coe_sort_eq_attach
{β : Type u}
{α : Type v}
(s : finset α)
[add_comm_monoid β]
(f : ↥s → β) :
theorem
finset.prod_coe_sort_eq_attach
{β : Type u}
{α : Type v}
(s : finset α)
[comm_monoid β]
(f : ↥s → β) :
theorem
finset.sum_coe_sort
{β : Type u}
{α : Type v}
(s : finset α)
(f : α → β)
[add_comm_monoid β] :
theorem
finset.prod_finset_coe
{β : Type u}
{α : Type v}
[comm_monoid β]
(f : α → β)
(s : finset α) :
theorem
finset.sum_finset_coe
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(f : α → β)
(s : finset α) :
theorem
finset.prod_apply_dite
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
[decidable_pred (λ (x : α), ¬p x)]
(f : Π (x : α), p x → γ)
(g : Π (x : α), ¬p x → γ)
(h : γ → β) :
∏ (x : α) in s, h (dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx)) = (∏ (x : {x // x ∈ finset.filter p s}) in (finset.filter p s).attach, h (f x.val _)) * ∏ (x : {x // x ∈ finset.filter (λ (x : α), ¬p x) s}) in (finset.filter (λ (x : α), ¬p x) s).attach, h (g x.val _)
theorem
finset.sum_apply_dite
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
[decidable_pred (λ (x : α), ¬p x)]
(f : Π (x : α), p x → γ)
(g : Π (x : α), ¬p x → γ)
(h : γ → β) :
∑ (x : α) in s, h (dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx)) = ∑ (x : {x // x ∈ finset.filter p s}) in (finset.filter p s).attach, h (f x.val _) + ∑ (x : {x // x ∈ finset.filter (λ (x : α), ¬p x) s}) in (finset.filter (λ (x : α), ¬p x) s).attach, h (g x.val _)
theorem
finset.prod_apply_ite
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → γ)
(h : γ → β) :
∏ (x : α) in s, h (ite (p x) (f x) (g x)) = (∏ (x : α) in finset.filter p s, h (f x)) * ∏ (x : α) in finset.filter (λ (x : α), ¬p x) s, h (g x)
theorem
finset.sum_apply_ite
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → γ)
(h : γ → β) :
∑ (x : α) in s, h (ite (p x) (f x) (g x)) = ∑ (x : α) in finset.filter p s, h (f x) + ∑ (x : α) in finset.filter (λ (x : α), ¬p x) s, h (g x)
theorem
finset.sum_dite
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
(f : Π (x : α), p x → β)
(g : Π (x : α), ¬p x → β) :
∑ (x : α) in s, dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx) = ∑ (x : {x // x ∈ finset.filter p s}) in (finset.filter p s).attach, f x.val _ + ∑ (x : {x // x ∈ finset.filter (λ (x : α), ¬p x) s}) in (finset.filter (λ (x : α), ¬p x) s).attach, g x.val _
theorem
finset.prod_dite
{β : Type u}
{α : Type v}
[comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
(f : Π (x : α), p x → β)
(g : Π (x : α), ¬p x → β) :
∏ (x : α) in s, dite (p x) (λ (hx : p x), f x hx) (λ (hx : ¬p x), g x hx) = (∏ (x : {x // x ∈ finset.filter p s}) in (finset.filter p s).attach, f x.val _) * ∏ (x : {x // x ∈ finset.filter (λ (x : α), ¬p x) s}) in (finset.filter (λ (x : α), ¬p x) s).attach, g x.val _
theorem
finset.prod_ite
{β : Type u}
{α : Type v}
[comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → β) :
∏ (x : α) in s, ite (p x) (f x) (g x) = (∏ (x : α) in finset.filter p s, f x) * ∏ (x : α) in finset.filter (λ (x : α), ¬p x) s, g x
theorem
finset.sum_ite
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{s : finset α}
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → β) :
∑ (x : α) in s, ite (p x) (f x) (g x) = ∑ (x : α) in finset.filter p s, f x + ∑ (x : α) in finset.filter (λ (x : α), ¬p x) s, g x
theorem
finset.prod_ite_of_false
{β : Type u}
{α : Type v}
{s : finset α}
[comm_monoid β]
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → β)
(h : ∀ (x : α), x ∈ s → ¬p x) :
theorem
finset.sum_ite_of_false
{β : Type u}
{α : Type v}
{s : finset α}
[add_comm_monoid β]
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → β)
(h : ∀ (x : α), x ∈ s → ¬p x) :
theorem
finset.prod_ite_of_true
{β : Type u}
{α : Type v}
{s : finset α}
[comm_monoid β]
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → β)
(h : ∀ (x : α), x ∈ s → p x) :
theorem
finset.sum_ite_of_true
{β : Type u}
{α : Type v}
{s : finset α}
[add_comm_monoid β]
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → β)
(h : ∀ (x : α), x ∈ s → p x) :
theorem
finset.sum_apply_ite_of_false
{β : Type u}
{α : Type v}
{γ : Type w}
{s : finset α}
[add_comm_monoid β]
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → γ)
(k : γ → β)
(h : ∀ (x : α), x ∈ s → ¬p x) :
theorem
finset.prod_apply_ite_of_false
{β : Type u}
{α : Type v}
{γ : Type w}
{s : finset α}
[comm_monoid β]
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → γ)
(k : γ → β)
(h : ∀ (x : α), x ∈ s → ¬p x) :
theorem
finset.sum_apply_ite_of_true
{β : Type u}
{α : Type v}
{γ : Type w}
{s : finset α}
[add_comm_monoid β]
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → γ)
(k : γ → β)
(h : ∀ (x : α), x ∈ s → p x) :
theorem
finset.prod_apply_ite_of_true
{β : Type u}
{α : Type v}
{γ : Type w}
{s : finset α}
[comm_monoid β]
{p : α → Prop}
{hp : decidable_pred p}
(f g : α → γ)
(k : γ → β)
(h : ∀ (x : α), x ∈ s → p x) :
theorem
finset.sum_extend_by_zero
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s : finset α)
(f : α → β) :
theorem
finset.prod_extend_by_one
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
(f : α → β) :
@[simp]
theorem
finset.sum_dite_eq
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : Π (x : α), a = x → β) :
@[simp]
theorem
finset.prod_dite_eq
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : Π (x : α), a = x → β) :
@[simp]
theorem
finset.prod_dite_eq'
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : Π (x : α), x = a → β) :
@[simp]
theorem
finset.sum_dite_eq'
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : Π (x : α), x = a → β) :
@[simp]
theorem
finset.prod_ite_eq
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : α → β) :
@[simp]
theorem
finset.sum_ite_eq
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : α → β) :
@[simp]
theorem
finset.sum_ite_eq'
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : α → β) :
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.
@[simp]
theorem
finset.prod_ite_eq'
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : α → β) :
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.
theorem
finset.sum_ite_index
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(p : Prop)
[decidable p]
(s t : finset α)
(f : α → β) :
theorem
finset.prod_ite_index
{β : Type u}
{α : Type v}
[comm_monoid β]
(p : Prop)
[decidable p]
(s t : finset α)
(f : α → β) :
@[simp]
theorem
finset.sum_dite_irrel
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(p : Prop)
[decidable p]
(s : finset α)
(f : p → α → β)
(g : ¬p → α → β) :
@[simp]
theorem
finset.prod_dite_irrel
{β : Type u}
{α : Type v}
[comm_monoid β]
(p : Prop)
[decidable p]
(s : finset α)
(f : p → α → β)
(g : ¬p → α → β) :
@[simp]
theorem
finset.sum_pi_single'
{ι : Type u_1}
{M : Type u_2}
[decidable_eq ι]
[add_comm_monoid M]
(i : ι)
(x : M)
(s : finset ι) :
@[simp]
theorem
finset.sum_pi_single
{ι : Type u_1}
{M : ι → Type u_2}
[decidable_eq ι]
[Π (i : ι), add_comm_monoid (M i)]
(i : ι)
(f : Π (i : ι), M i)
(s : finset ι) :
theorem
finset.prod_bij_ne_one
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
{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₁ : a ∈ s) (h₂ : f a ≠ 1), b = i a h₁ h₂))
(h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)) :
∏ (x : α) in s, f x = ∏ (x : γ) in t, g x
theorem
finset.sum_bij_ne_zero
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
{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₁ : a ∈ s) (h₂ : f a ≠ 0), b = i a h₁ h₂))
(h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), f a = g (i a h₁ h₂)) :
∑ (x : α) in s, f x = ∑ (x : γ) in t, g x
theorem
finset.sum_dite_of_false
{β : Type u}
{α : Type v}
{s : finset α}
[add_comm_monoid β]
{p : α → Prop}
{hp : decidable_pred p}
(h : ∀ (x : α), x ∈ s → ¬p x)
(f : Π (x : α), p x → β)
(g : Π (x : α), ¬p x → β) :
theorem
finset.prod_dite_of_false
{β : Type u}
{α : Type v}
{s : finset α}
[comm_monoid β]
{p : α → Prop}
{hp : decidable_pred p}
(h : ∀ (x : α), x ∈ s → ¬p x)
(f : Π (x : α), p x → β)
(g : Π (x : α), ¬p x → β) :
theorem
finset.sum_dite_of_true
{β : Type u}
{α : Type v}
{s : finset α}
[add_comm_monoid β]
{p : α → Prop}
{hp : decidable_pred p}
(h : ∀ (x : α), x ∈ s → p x)
(f : Π (x : α), p x → β)
(g : Π (x : α), ¬p x → β) :
theorem
finset.prod_dite_of_true
{β : Type u}
{α : Type v}
{s : finset α}
[comm_monoid β]
{p : α → Prop}
{hp : decidable_pred p}
(h : ∀ (x : α), x ∈ s → p x)
(f : Π (x : α), p x → β)
(g : Π (x : α), ¬p x → β) :
theorem
finset.nonempty_of_sum_ne_zero
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[add_comm_monoid β]
(h : ∑ (x : α) in s, f x ≠ 0) :
s.nonempty
theorem
finset.nonempty_of_prod_ne_one
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[comm_monoid β]
(h : ∏ (x : α) in s, f x ≠ 1) :
s.nonempty
theorem
finset.exists_ne_zero_of_sum_ne_zero
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[add_comm_monoid β]
(h : ∑ (x : α) in s, f x ≠ 0) :
theorem
finset.exists_ne_one_of_prod_ne_one
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[comm_monoid β]
(h : ∏ (x : α) in s, f x ≠ 1) :
theorem
finset.prod_range_succ_comm
{β : Type u}
[comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
∏ (x : ℕ) in finset.range (n + 1), f x = (f n) * ∏ (x : ℕ) in finset.range n, f x
theorem
finset.sum_range_succ_comm
{β : Type u}
[add_comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
∑ (x : ℕ) in finset.range (n + 1), f x = f n + ∑ (x : ℕ) in finset.range n, f x
theorem
finset.prod_range_succ
{β : Type u}
[comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
∏ (x : ℕ) in finset.range (n + 1), f x = (∏ (x : ℕ) in finset.range n, f x) * f n
theorem
finset.sum_range_succ
{β : Type u}
[add_comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
∑ (x : ℕ) in finset.range (n + 1), f x = ∑ (x : ℕ) in finset.range n, f x + f n
theorem
finset.prod_range_succ'
{β : Type u}
[comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
∏ (k : ℕ) in finset.range (n + 1), f k = (∏ (k : ℕ) in finset.range n, f (k + 1)) * f 0
theorem
finset.sum_range_succ'
{β : Type u}
[add_comm_monoid β]
(f : ℕ → β)
(n : ℕ) :
∑ (k : ℕ) in finset.range (n + 1), f k = ∑ (k : ℕ) in finset.range n, f (k + 1) + f 0
theorem
finset.eventually_constant_sum
{β : Type u}
[add_comm_monoid β]
{u : ℕ → β}
{N : ℕ}
(hu : ∀ (n : ℕ), n ≥ N → u n = 0)
{n : ℕ}
(hn : N ≤ n) :
∑ (k : ℕ) in finset.range (n + 1), u k = ∑ (k : ℕ) in finset.range (N + 1), u k
theorem
finset.eventually_constant_prod
{β : Type u}
[comm_monoid β]
{u : ℕ → β}
{N : ℕ}
(hu : ∀ (n : ℕ), n ≥ N → u n = 1)
{n : ℕ}
(hn : N ≤ n) :
∏ (k : ℕ) in finset.range (n + 1), u k = ∏ (k : ℕ) in finset.range (N + 1), u k
theorem
finset.prod_range_add
{β : Type u}
[comm_monoid β]
(f : ℕ → β)
(n m : ℕ) :
∏ (x : ℕ) in finset.range (n + m), f x = (∏ (x : ℕ) in finset.range n, f x) * ∏ (x : ℕ) in finset.range m, f (n + x)
theorem
finset.sum_range_add
{β : Type u}
[add_comm_monoid β]
(f : ℕ → β)
(n m : ℕ) :
∑ (x : ℕ) in finset.range (n + m), f x = ∑ (x : ℕ) in finset.range n, f x + ∑ (x : ℕ) in finset.range m, f (n + x)
theorem
finset.sum_range_add_sub_sum_range
{α : Type u_1}
[add_comm_group α]
(f : ℕ → α)
(n m : ℕ) :
∑ (k : ℕ) in finset.range (n + m), f k - ∑ (k : ℕ) in finset.range n, f k = ∑ (k : ℕ) in finset.range m, f (n + k)
theorem
finset.prod_range_add_div_prod_range
{α : Type u_1}
[comm_group α]
(f : ℕ → α)
(n m : ℕ) :
(∏ (k : ℕ) in finset.range (n + m), f k) / ∏ (k : ℕ) in finset.range n, f k = ∏ (k : ℕ) in finset.range m, f (n + k)
theorem
finset.sum_range_zero
{β : Type u}
[add_comm_monoid β]
(f : ℕ → β) :
∑ (k : ℕ) in finset.range 0, f k = 0
theorem
finset.prod_range_zero
{β : Type u}
[comm_monoid β]
(f : ℕ → β) :
∏ (k : ℕ) in finset.range 0, f k = 1
theorem
finset.sum_range_one
{β : Type u}
[add_comm_monoid β]
(f : ℕ → β) :
∑ (k : ℕ) in finset.range 1, f k = f 0
theorem
finset.prod_range_one
{β : Type u}
[comm_monoid β]
(f : ℕ → β) :
∏ (k : ℕ) in finset.range 1, f k = f 0
theorem
finset.prod_multiset_map_count
{α : Type v}
[decidable_eq α]
(s : multiset α)
{M : Type u_1}
[comm_monoid M]
(f : α → M) :
(multiset.map f s).prod = ∏ (m : α) in s.to_finset, f m ^ multiset.count m s
theorem
finset.sum_multiset_map_count
{α : Type v}
[decidable_eq α]
(s : multiset α)
{M : Type u_1}
[add_comm_monoid M]
(f : α → M) :
(multiset.map f s).sum = ∑ (m : α) in s.to_finset, multiset.count m s • f m
theorem
finset.sum_multiset_count
{α : Type v}
[decidable_eq α]
[add_comm_monoid α]
(s : multiset α) :
s.sum = ∑ (m : α) in s.to_finset, multiset.count m s • m
theorem
finset.prod_multiset_count
{α : Type v}
[decidable_eq α]
[comm_monoid α]
(s : multiset α) :
s.prod = ∏ (m : α) in s.to_finset, m ^ multiset.count m s
theorem
finset.prod_multiset_count_of_subset
{α : Type v}
[decidable_eq α]
[comm_monoid α]
(m : multiset α)
(s : finset α)
(hs : m.to_finset ⊆ s) :
m.prod = ∏ (i : α) in s, i ^ multiset.count i m
theorem
finset.sum_multiset_count_of_subset
{α : Type v}
[decidable_eq α]
[add_comm_monoid α]
(m : multiset α)
(s : finset α)
(hs : m.to_finset ⊆ s) :
m.sum = ∑ (i : α) in s, multiset.count i m • i
theorem
finset.sum_mem_multiset
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(m : multiset α)
(f : {x // x ∈ m} → β)
(g : α → β)
(hfg : ∀ (x : {x // x ∈ m}), f x = g ↑x) :
theorem
finset.prod_mem_multiset
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(m : multiset α)
(f : {x // x ∈ m} → β)
(g : α → β)
(hfg : ∀ (x : {x // x ∈ m}), f x = g ↑x) :
theorem
finset.prod_induction
{α : Type v}
{s : finset α}
{M : Type u_1}
[comm_monoid M]
(f : α → M)
(p : M → Prop)
(p_mul : ∀ (a b : M), p a → p b → p (a * b))
(p_one : p 1)
(p_s : ∀ (x : α), x ∈ s → p (f x)) :
p (∏ (x : α) in s, f x)
To prove a property of a product, it suffices to prove that the property is multiplicative and holds on factors.
theorem
finset.sum_induction
{α : Type v}
{s : finset α}
{M : Type u_1}
[add_comm_monoid M]
(f : α → M)
(p : M → Prop)
(p_mul : ∀ (a b : M), p a → p b → p (a + b))
(p_one : p 0)
(p_s : ∀ (x : α), x ∈ s → p (f x)) :
p (∑ (x : α) in s, f x)
To prove a property of a sum, it suffices to prove that the property is additive and holds on summands.
theorem
finset.sum_induction_nonempty
{α : Type v}
{s : finset α}
{M : Type u_1}
[add_comm_monoid M]
(f : α → M)
(p : M → Prop)
(p_mul : ∀ (a b : M), p a → p b → p (a + b))
(hs_nonempty : s.nonempty)
(p_s : ∀ (x : α), x ∈ s → p (f x)) :
p (∑ (x : α) in s, f x)
To prove a property of a sum, it suffices to prove that the property is additive and holds on summands.
theorem
finset.prod_induction_nonempty
{α : Type v}
{s : finset α}
{M : Type u_1}
[comm_monoid M]
(f : α → M)
(p : M → Prop)
(p_mul : ∀ (a b : M), p a → p b → p (a * b))
(hs_nonempty : s.nonempty)
(p_s : ∀ (x : α), x ∈ s → p (f x)) :
p (∏ (x : α) in s, f x)
To prove a property of a product, it suffices to prove that the property is multiplicative and holds on factors.
theorem
finset.prod_range_induction
{M : Type u_1}
[comm_monoid M]
(f s : ℕ → M)
(h0 : s 0 = 1)
(h : ∀ (n : ℕ), s (n + 1) = (s n) * f n)
(n : ℕ) :
∏ (k : ℕ) in finset.range n, f k = s n
For any product along {0, ..., n-1} of a commutative-monoid-valued function, we can verify that
it's equal to a different function just by checking ratios of adjacent terms.
This is a multiplicative discrete analogue of the fundamental theorem of calculus.
theorem
finset.sum_range_induction
{M : Type u_1}
[add_comm_monoid M]
(f s : ℕ → M)
(h0 : s 0 = 0)
(h : ∀ (n : ℕ), s (n + 1) = s n + f n)
(n : ℕ) :
∑ (k : ℕ) in finset.range n, f k = s n
For any sum along {0, ..., n-1} of a commutative-monoid-valued function,
we can verify that it's equal to a different function
just by checking differences of adjacent terms.
This is a discrete analogue
of the fundamental theorem of calculus.
A telescoping sum along {0, ..., n - 1} of an additive commutative group valued function
reduces to the difference of the last and first terms.
A telescoping product along {0, ..., n - 1} of a commutative group valued function reduces to
the ratio of the last and first factors.
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.
@[simp]
@[simp]
theorem
finset.nsmul_eq_sum_const
{β : Type u}
[add_comm_monoid β]
(b : β)
(n : ℕ) :
n • b = ∑ (k : ℕ) in finset.range n, b
theorem
finset.pow_eq_prod_const
{β : Type u}
[comm_monoid β]
(b : β)
(n : ℕ) :
b ^ n = ∏ (k : ℕ) in finset.range n, b
theorem
finset.sum_nsmul
{β : Type u}
{α : Type v}
[add_comm_monoid β]
(s : finset α)
(n : ℕ)
(f : α → β) :
theorem
finset.prod_pow
{β : Type u}
{α : Type v}
[comm_monoid β]
(s : finset α)
(n : ℕ)
(f : α → β) :
theorem
finset.prod_flip
{β : Type u}
[comm_monoid β]
{n : ℕ}
(f : ℕ → β) :
∏ (r : ℕ) in finset.range (n + 1), f (n - r) = ∏ (k : ℕ) in finset.range (n + 1), f k
theorem
finset.sum_flip
{β : Type u}
[add_comm_monoid β]
{n : ℕ}
(f : ℕ → β) :
∑ (r : ℕ) in finset.range (n + 1), f (n - r) = ∑ (k : ℕ) in finset.range (n + 1), f k
theorem
finset.prod_involution
{β : Type u}
{α : Type v}
[comm_monoid β]
{s : finset α}
{f : α → β}
(g : Π (a : α), a ∈ s → α)
(h : ∀ (a : α) (ha : a ∈ s), (f a) * f (g a ha) = 1)
(g_ne : ∀ (a : α) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a)
(g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s)
(g_inv : ∀ (a : α) (ha : a ∈ s), g (g a ha) _ = a) :
∏ (x : α) in s, f x = 1
theorem
finset.sum_involution
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{s : finset α}
{f : α → β}
(g : Π (a : α), a ∈ s → α)
(h : ∀ (a : α) (ha : a ∈ s), f a + f (g a ha) = 0)
(g_ne : ∀ (a : α) (ha : a ∈ s), f a ≠ 0 → g a ha ≠ a)
(g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s)
(g_inv : ∀ (a : α) (ha : a ∈ s), g (g a ha) _ = a) :
∑ (x : α) in s, f x = 0
theorem
finset.prod_comp
{β : Type u}
{α : Type v}
{γ : Type w}
{s : finset α}
[comm_monoid β]
[decidable_eq γ]
(f : γ → β)
(g : α → γ) :
∏ (a : α) in s, f (g a) = ∏ (b : γ) in finset.image g s, f b ^ (finset.filter (λ (a : α), g a = b) s).card
The product of the composition of functions f and g, is the product over b ∈ s.image g of
f b to the power of the cardinality of the fibre of b. See also finset.prod_image.
theorem
finset.sum_comp
{β : Type u}
{α : Type v}
{γ : Type w}
{s : finset α}
[add_comm_monoid β]
[decidable_eq γ]
(f : γ → β)
(g : α → γ) :
∑ (a : α) in s, f (g a) = ∑ (b : γ) in finset.image g s, (finset.filter (λ (a : α), g a = b) s).card • f b
The sum of the composition of functions f and g, is the sum over b ∈ s.image g
of f b times of the cardinality of the fibre of b. See also finset.sum_image.
theorem
finset.sum_piecewise
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s t : finset α)
(f g : α → β) :
theorem
finset.prod_piecewise
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s t : finset α)
(f g : α → β) :
theorem
finset.prod_inter_mul_prod_diff
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s t : finset α)
(f : α → β) :
theorem
finset.sum_inter_add_sum_diff
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s t : finset α)
(f : α → β) :
theorem
finset.prod_eq_mul_prod_diff_singleton
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
{s : finset α}
{i : α}
(h : i ∈ s)
(f : α → β) :
theorem
finset.sum_eq_add_sum_diff_singleton
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
{s : finset α}
{i : α}
(h : i ∈ s)
(f : α → β) :
theorem
finset.prod_eq_prod_diff_singleton_mul
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
{s : finset α}
{i : α}
(h : i ∈ s)
(f : α → β) :
theorem
finset.sum_eq_sum_diff_singleton_add
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
{s : finset α}
{i : α}
(h : i ∈ s)
(f : α → β) :
theorem
fintype.prod_eq_mul_prod_compl
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
[fintype α]
(a : α)
(f : α → β) :
theorem
fintype.sum_eq_add_sum_compl
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
[fintype α]
(a : α)
(f : α → β) :
theorem
fintype.prod_eq_prod_compl_mul
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
[fintype α]
(a : α)
(f : α → β) :
theorem
fintype.sum_eq_sum_compl_add
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
[fintype α]
(a : α)
(f : α → β) :
theorem
finset.dvd_prod_of_mem
{β : Type u}
{α : Type v}
[comm_monoid β]
(f : α → β)
{a : α}
{s : finset α}
(ha : a ∈ s) :
f a ∣ ∏ (i : α) in s, f i
theorem
finset.sum_partition
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[add_comm_monoid β]
(R : setoid α)
[decidable_rel setoid.r] :
∑ (x : α) in s, f x = ∑ (xbar : quotient R) in finset.image quotient.mk s, ∑ (y : α) in finset.filter (λ (y : α), ⟦y⟧ = xbar) s, f y
A sum can be partitioned into a sum of sums, each equivalent under a setoid.
theorem
finset.prod_partition
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[comm_monoid β]
(R : setoid α)
[decidable_rel setoid.r] :
∏ (x : α) in s, f x = ∏ (xbar : quotient R) in finset.image quotient.mk s, ∏ (y : α) in finset.filter (λ (y : α), ⟦y⟧ = xbar) s, f y
A product can be partitioned into a product of products, each equivalent under a setoid.
theorem
finset.prod_cancels_of_partition_cancels
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[comm_monoid β]
(R : setoid α)
[decidable_rel setoid.r]
(h : ∀ (x : α), x ∈ s → ∏ (a : α) in finset.filter (λ (y : α), y ≈ x) s, f a = 1) :
∏ (x : α) in s, f x = 1
If we can partition a product into subsets that cancel out, then the whole product cancels.
theorem
finset.sum_cancels_of_partition_cancels
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[add_comm_monoid β]
(R : setoid α)
[decidable_rel setoid.r]
(h : ∀ (x : α), x ∈ s → ∑ (a : α) in finset.filter (λ (y : α), y ≈ x) s, f a = 0) :
∑ (x : α) in s, f x = 0
If we can partition a sum into subsets that cancel out, then the whole sum cancels.
theorem
finset.prod_update_of_not_mem
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
{s : finset α}
{i : α}
(h : i ∉ s)
(f : α → β)
(b : β) :
∏ (x : α) in s, function.update f i b x = ∏ (x : α) in s, f x
theorem
finset.sum_update_of_not_mem
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
{s : finset α}
{i : α}
(h : i ∉ s)
(f : α → β)
(b : β) :
∑ (x : α) in s, function.update f i b x = ∑ (x : α) in s, f x
theorem
finset.prod_update_of_mem
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
{s : finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
(b : β) :
∏ (x : α) in s, function.update f i b x = b * ∏ (x : α) in s \ {i}, f x
theorem
finset.sum_update_of_mem
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
{s : finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
(b : β) :
∑ (x : α) in s, function.update f i b x = b + ∑ (x : α) in s \ {i}, f x
theorem
finset.eq_of_card_le_one_of_sum_eq
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{s : finset α}
(hc : s.card ≤ 1)
{f : α → β}
{b : β}
(h : ∑ (x : α) in s, f x = b)
(x : α)
(H : x ∈ s) :
f x = b
If a sum of a finset of size at most 1 has a given
value, so do the terms in that sum.
theorem
finset.eq_of_card_le_one_of_prod_eq
{β : Type u}
{α : Type v}
[comm_monoid β]
{s : finset α}
(hc : s.card ≤ 1)
{f : α → β}
{b : β}
(h : ∏ (x : α) in s, f x = b)
(x : α)
(H : x ∈ s) :
f x = b
If a product of a finset of size at most 1 has a given value, so
do the terms in that product.
theorem
finset.add_sum_erase
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s : finset α)
(f : α → β)
{a : α}
(h : a ∈ s) :
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.
theorem
finset.mul_prod_erase
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
(f : α → β)
{a : α}
(h : a ∈ s) :
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.
theorem
finset.sum_erase_add
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s : finset α)
(f : α → β)
{a : α}
(h : a ∈ s) :
A variant of finset.add_sum_erase with the addition swapped.
theorem
finset.prod_erase_mul
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
(f : α → β)
{a : α}
(h : a ∈ s) :
A variant of finset.mul_prod_erase with the multiplication swapped.
theorem
finset.prod_erase
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
{f : α → β}
{a : α}
(h : f a = 1) :
If a function applied at a point is 1, a product is unchanged by
removing that point, if present, from a finset.
theorem
finset.sum_erase
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[decidable_eq α]
(s : finset α)
{f : α → β}
{a : α}
(h : f a = 0) :
If a function applied at a point is 0, a sum is unchanged by
removing that point, if present, from a finset.
theorem
finset.eq_zero_of_sum_eq_zero
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{s : finset α}
{f : α → β}
{a : α}
(hp : ∑ (x : α) in s, f x = 0)
(h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 0)
(x : α)
(H : x ∈ s) :
f x = 0
If a sum is 0 and the function is 0 except possibly at one
point, it is 0 everywhere on the finset.
theorem
finset.eq_one_of_prod_eq_one
{β : Type u}
{α : Type v}
[comm_monoid β]
{s : finset α}
{f : α → β}
{a : α}
(hp : ∏ (x : α) in s, f x = 1)
(h1 : ∀ (x : α), x ∈ s → x ≠ a → f x = 1)
(x : α)
(H : x ∈ s) :
f x = 1
If a product is 1 and the function is 1 except possibly at one
point, it is 1 everywhere on the finset.
theorem
finset.prod_pow_boole
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
(f : α → β)
(a : α) :
theorem
finset.prod_dvd_prod_of_dvd
{β : Type u}
{α : Type v}
[comm_monoid β]
{S : finset α}
(g1 g2 : α → β)
(h : ∀ (a : α), a ∈ S → g1 a ∣ g2 a) :
theorem
finset.prod_dvd_prod_of_subset
{ι : Type u_1}
{M : Type u_2}
[comm_monoid M]
(s t : finset ι)
(f : ι → M)
(h : s ⊆ t) :
∏ (i : ι) in s, f i ∣ ∏ (i : ι) in t, f i
theorem
finset.prod_add_prod_eq
{β : Type u}
{α : Type v}
[comm_semiring β]
{s : finset α}
{i : α}
{f g h : α → β}
(hi : i ∈ s)
(h1 : g i + h i = f i)
(h2 : ∀ (j : α), j ∈ s → j ≠ i → g j = f j)
(h3 : ∀ (j : α), j ∈ s → j ≠ i → h j = f j) :
If f = g = h everywhere but at i, where f i = g i + h i, then the product of f over s
is the sum of the products of g and h.
@[simp]
theorem
finset.sum_boole
{β : Type u}
{α : Type v}
{s : finset α}
{p : α → Prop}
[non_assoc_semiring β]
{hp : decidable_pred p} :
∑ (x : α) in s, ite (p x) 1 0 = ↑((finset.filter p s).card)
theorem
commute.sum_right
{β : Type u}
{α : Type v}
[non_unital_non_assoc_semiring β]
(s : finset α)
(f : α → β)
(b : β)
(h : ∀ (i : α), i ∈ s → commute b (f i)) :
commute b (∑ (i : α) in s, f i)
theorem
commute.sum_left
{β : Type u}
{α : Type v}
[non_unital_non_assoc_semiring β]
(s : finset α)
(f : α → β)
(b : β)
(h : ∀ (i : α), i ∈ s → commute (f i) b) :
commute (∑ (i : α) in s, f i) b
@[simp]
theorem
finset.op_sum
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{s : finset α}
(f : α → β) :
mul_opposite.op (∑ (x : α) in s, f x) = ∑ (x : α) in s, mul_opposite.op (f x)
Moving to the opposite additive commutative monoid commutes with summing.
@[simp]
theorem
finset.unop_sum
{β : Type u}
{α : Type v}
[add_comm_monoid β]
{s : finset α}
(f : α → βᵐᵒᵖ) :
mul_opposite.unop (∑ (x : α) in s, f x) = ∑ (x : α) in s, mul_opposite.unop (f x)
@[simp]
theorem
finset.sum_neg_distrib
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[add_comm_group β] :
@[simp]
theorem
finset.prod_inv_distrib
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[comm_group β] :
theorem
finset.zsmul_sum
{β : Type u}
{α : Type v}
[add_comm_group β]
(f : α → β)
(s : finset α)
(n : ℤ) :
theorem
finset.prod_zpow
{β : Type u}
{α : Type v}
[comm_group β]
(f : α → β)
(s : finset α)
(n : ℤ) :
theorem
finset.prod_sdiff_div_prod_sdiff
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[comm_group β]
[decidable_eq α] :
theorem
finset.sum_sdiff_sub_sum_sdiff
{β : Type u}
{α : Type v}
{s₁ s₂ : finset α}
{f : α → β}
[add_comm_group β]
[decidable_eq α] :
theorem
finset.card_bUnion_le
{β : Type u}
{α : Type v}
[decidable_eq β]
{s : finset α}
{t : α → finset β} :
theorem
finset.card_eq_sum_card_fiberwise
{β : Type u}
{α : Type v}
[decidable_eq β]
{f : α → β}
{s : finset α}
{t : finset β}
(H : ∀ (x : α), x ∈ s → f x ∈ t) :
s.card = ∑ (a : β) in t, (finset.filter (λ (x : α), f x = a) s).card
theorem
finset.card_eq_sum_card_image
{β : Type u}
{α : Type v}
[decidable_eq β]
(f : α → β)
(s : finset α) :
s.card = ∑ (a : β) in finset.image f s, (finset.filter (λ (x : α), f x = a) s).card
@[simp]
theorem
finset.sum_sub_distrib
{β : Type u}
{α : Type v}
{s : finset α}
{f g : α → β}
[add_comm_group β] :
theorem
finset.prod_eq_zero
{β : Type u}
{α : Type v}
{s : finset α}
{a : α}
{f : α → β}
[comm_monoid_with_zero β]
(ha : a ∈ s)
(h : f a = 0) :
∏ (x : α) in s, f x = 0
theorem
finset.prod_boole
{β : Type u}
{α : Type v}
[comm_monoid_with_zero β]
{s : finset α}
{p : α → Prop}
[decidable_pred p] :
theorem
finset.prod_eq_zero_iff
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[comm_monoid_with_zero β]
[nontrivial β]
[no_zero_divisors β] :
theorem
finset.prod_ne_zero_iff
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[comm_monoid_with_zero β]
[nontrivial β]
[no_zero_divisors β] :
@[simp]
theorem
finset.prod_inv_distrib'
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[comm_group_with_zero β] :
theorem
finset.prod_unique_nonempty
{α : Type u_1}
{β : Type u_2}
[comm_monoid β]
[unique α]
(s : finset α)
(f : α → β)
(h : s.nonempty) :
theorem
finset.sum_unique_nonempty
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid β]
[unique α]
(s : finset α)
(f : α → β)
(h : s.nonempty) :
theorem
fintype.sum_bijective
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[fintype α]
[fintype β]
[add_comm_monoid M]
(e : α → β)
(he : function.bijective e)
(f : α → M)
(g : β → M)
(h : ∀ (x : α), f x = g (e x)) :
∑ (x : α), f x = ∑ (x : β), g x
fintype.sum_equiv is a variant of finset.sum_bij that accepts
function.bijective.
See function.bijective.sum_comp for a version without h.
theorem
fintype.prod_bijective
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[fintype α]
[fintype β]
[comm_monoid M]
(e : α → β)
(he : function.bijective e)
(f : α → M)
(g : β → M)
(h : ∀ (x : α), f x = g (e x)) :
∏ (x : α), f x = ∏ (x : β), g x
fintype.prod_bijective is a variant of finset.prod_bij that accepts function.bijective.
See function.bijective.prod_comp for a version without h.
theorem
fintype.prod_equiv
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[fintype α]
[fintype β]
[comm_monoid M]
(e : α ≃ β)
(f : α → M)
(g : β → M)
(h : ∀ (x : α), f x = g (⇑e x)) :
∏ (x : α), f x = ∏ (x : β), g x
fintype.prod_equiv is a specialization of finset.prod_bij that
automatically fills in most arguments.
See equiv.prod_comp for a version without h.
theorem
fintype.sum_equiv
{α : Type u_1}
{β : Type u_2}
{M : Type u_3}
[fintype α]
[fintype β]
[add_comm_monoid M]
(e : α ≃ β)
(f : α → M)
(g : β → M)
(h : ∀ (x : α), f x = g (⇑e x)) :
∑ (x : α), f x = ∑ (x : β), g x
fintype.sum_equiv is a specialization of finset.sum_bij that
automatically fills in most arguments.
See equiv.sum_comp for a version without h.
theorem
fintype.sum_unique
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid β]
[unique α]
(f : α → β) :
theorem
fintype.prod_empty
{α : Type u_1}
{β : Type u_2}
[comm_monoid β]
[is_empty α]
(f : α → β) :
∏ (x : α), f x = 1
theorem
fintype.sum_empty
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid β]
[is_empty α]
(f : α → β) :
∑ (x : α), f x = 0
theorem
fintype.prod_subsingleton
{α : Type u_1}
{β : Type u_2}
[comm_monoid β]
[subsingleton α]
(f : α → β)
(a : α) :
∏ (x : α), f x = f a
theorem
fintype.sum_subsingleton
{α : Type u_1}
{β : Type u_2}
[add_comm_monoid β]
[subsingleton α]
(f : α → β)
(a : α) :
∑ (x : α), f x = f a
theorem
fintype.prod_subtype_mul_prod_subtype
{α : Type u_1}
{β : Type u_2}
[fintype α]
[comm_monoid β]
(p : α → Prop)
(f : α → β)
[decidable_pred p] :
theorem
fintype.sum_subtype_add_sum_subtype
{α : Type u_1}
{β : Type u_2}
[fintype α]
[add_comm_monoid β]
(p : α → Prop)
(f : α → β)
[decidable_pred p] :
theorem
list.sum_to_finset
{α : Type v}
{M : Type u_1}
[decidable_eq α]
[add_comm_monoid M]
(f : α → M)
{l : list α}
(hl : l.nodup) :
theorem
list.prod_to_finset
{α : Type v}
{M : Type u_1}
[decidable_eq α]
[comm_monoid M]
(f : α → M)
{l : list α}
(hl : l.nodup) :
@[simp]
theorem
multiset.to_finset_sum_count_eq
{α : Type v}
[decidable_eq α]
(s : multiset α) :
∑ (a : α) in s.to_finset, multiset.count a s = ⇑multiset.card s
theorem
multiset.count_sum'
{β : Type u}
{α : Type v}
[decidable_eq α]
{s : finset β}
{a : α}
{f : β → multiset α} :
multiset.count a (∑ (x : β) in s, f x) = ∑ (x : β) in s, multiset.count a (f x)
@[simp]
theorem
multiset.to_finset_sum_count_nsmul_eq
{α : Type v}
[decidable_eq α]
(s : multiset α) :
∑ (a : α) in s.to_finset, multiset.count a s • {a} = s
theorem
multiset.exists_smul_of_dvd_count
{α : Type v}
[decidable_eq α]
(s : multiset α)
{k : ℕ}
(h : ∀ (a : α), a ∈ s → k ∣ multiset.count a s) :
theorem
multiset.to_finset_prod_dvd_prod
{α : Type v}
[decidable_eq α]
[comm_monoid α]
(S : multiset α) :
theorem
multiset.sum_sum
{α : Type u_1}
{ι : Type u_2}
[add_comm_monoid α]
(f : ι → multiset α)
(s : finset ι) :
theorem
multiset.prod_sum
{α : Type u_1}
{ι : Type u_2}
[comm_monoid α]
(f : ι → multiset α)
(s : finset ι) :
@[simp, norm_cast]
theorem
nat.cast_sum
{β : Type u}
{α : Type v}
[add_comm_monoid β]
[has_one β]
(s : finset α)
(f : α → ℕ) :
@[simp, norm_cast]
theorem
int.cast_sum
{β : Type u}
{α : Type v}
[add_comm_group β]
[has_one β]
(s : finset α)
(f : α → ℤ) :
@[simp, norm_cast]
@[simp, norm_cast]