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
add_monoid_hom.map_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
[add_comm_monoid γ]
(g : β →+ γ)
(f : α → β)
(s : finset α) :
theorem
monoid_hom.map_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
[comm_monoid γ]
(g : β →* γ)
(f : α → β)
(s : finset α) :
theorem
add_equiv.map_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[add_comm_monoid β]
[add_comm_monoid γ]
(g : β ≃+ γ)
(f : α → β)
(s : finset α) :
theorem
mul_equiv.map_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_monoid β]
[comm_monoid γ]
(g : β ≃* γ)
(f : α → β)
(s : finset α) :
theorem
ring_hom.map_list_sum
{β : Type u}
{γ : Type w}
[non_assoc_semiring β]
[non_assoc_semiring γ]
(f : β →+* γ)
(l : list β) :
theorem
ring_hom.map_multiset_prod
{β : Type u}
{γ : Type w}
[comm_semiring β]
[comm_semiring γ]
(f : β →+* γ)
(s : multiset β) :
theorem
ring_hom.map_multiset_sum
{β : Type u}
{γ : Type w}
[non_assoc_semiring β]
[non_assoc_semiring γ]
(f : β →+* γ)
(s : multiset β) :
theorem
ring_hom.map_prod
{β : Type u}
{α : Type v}
{γ : Type w}
[comm_semiring β]
[comm_semiring γ]
(g : β →+* γ)
(f : α → β)
(s : finset α) :
theorem
ring_hom.map_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[non_assoc_semiring β]
[non_assoc_semiring γ]
(g : β →+* γ)
(f : α → β)
(s : finset α) :
theorem
add_monoid_hom.coe_sum
{β : Type u}
{α : Type v}
{γ : Type w}
[add_zero_class β]
[add_comm_monoid γ]
(f : α → β →+ γ)
(s : finset α) :
theorem
monoid_hom.coe_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
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_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.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.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.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.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 : α → β) :
@[simp]
theorem
finset.prod_ite_eq'
{β : Type u}
{α : Type v}
[comm_monoid β]
[decidable_eq α]
(s : finset α)
(a : α)
(b : α → β) :
When a product is taken over a conditional whose condition is an equality test on the index
and whose alternative is 1, then the product's value is either the term at that index or 1.
The difference with 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.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_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.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.pow_eq_prod_const
{β : Type u}
[comm_monoid β]
(b : β)
(n : ℕ) :
b ^ n = ∏ (k : ℕ) in finset.range n, b
theorem
finset.pow_eq_sum_const
{β : Type u}
[add_comm_monoid β]
(b : β)
(n : ℕ) :
n • b = ∑ (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_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_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
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
@[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.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.prod_finset_coe
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[comm_monoid β] :
theorem
fintype.sum_finset_coe
{β : Type u}
{α : Type v}
{s : finset α}
{f : α → β}
[add_comm_monoid β] :
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) :
@[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]
theorem
units.coe_prod
{α : Type v}
{M : Type u_1}
[comm_monoid M]
(f : α → units M)
(s : finset α) :