Big operators #
In this file we define products and sums indexed by finite sets (specifically, Finset).
Notation #
We introduce the following notation.
Let s be a Finset α, and f : α → β a function.
∏ x ∈ s, f xis notation forFinset.prod s f(assumingβis aCommMonoid)∑ x ∈ s, f xis notation forFinset.sum s f(assumingβis anAddCommMonoid)∏ x, f xis notation forFinset.prod Finset.univ f(assumingαis aFintypeandβis aCommMonoid)∑ x, f xis notation forFinset.sum Finset.univ f(assumingαis aFintypeandβis anAddCommMonoid)
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.
∏ x ∈ s, f x is the product of f x as x ranges over the elements of the finite set s.
When the index type is a Fintype, the notation ∏ x, f x, is a shorthand for
∏ x ∈ Finset.univ, f x.
Equations
- s.prod f = (Multiset.map f s.val).prod
Instances For
∑ x ∈ s, f x is the sum of f x as x ranges over the elements
of the finite set s.
When the index type is a Fintype, the notation ∑ x, f x, is a shorthand for
∑ x ∈ Finset.univ, f x.
Equations
- s.sum f = (Multiset.map f s.val).sum
Instances For
@[simp]
theorem
Finset.prod_mk
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(s : Multiset α)
(hs : s.Nodup)
(f : α → β)
:
{ val := s, nodup := hs }.prod f = (Multiset.map f s).prod
@[simp]
theorem
Finset.sum_mk
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Multiset α)
(hs : s.Nodup)
(f : α → β)
:
{ val := s, nodup := hs }.sum f = (Multiset.map f s).sum
@[simp]
@[simp]
A bigOpBinder is like an extBinder and has the form x, x : ty, or x pred
where pred is a binderPred like < 2.
Unlike extBinder, x is a term.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A BigOperator binder in parentheses
Equations
- One or more equations did not get rendered due to their size.
Instances For
A list of parenthesized binders
Equations
- One or more equations did not get rendered due to their size.
Instances For
A single (unparenthesized) binder, or a list of parenthesized binders
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
BigOperators.processBigOpBinder
(processed : Array (Lean.Term × Lean.Term))
(binder : Lean.TSyntax `BigOperators.bigOpBinder)
:
Collects additional binder/Finset pairs for the given bigOpBinder.
Note: this is not extensible at the moment, unlike the usual bigOpBinder expansions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Collects the binder/Finset pairs for the given bigOpBinders.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Collect the binderIdents into a ⟨...⟩ expression.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Collect the terms into a product of sets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
∑ x, f xis notation forFinset.sum Finset.univ f. It is the sum off x, wherexranges over the finite domain off.∑ x ∈ s, f xis notation forFinset.sum s f. It is the sum off x, wherexranges over the finite sets(either aFinsetor aSetwith aFintypeinstance).∑ x ∈ s with p x, f xis notation forFinset.sum (Finset.filter p s) f.∑ (x ∈ s) (y ∈ t), f x yis notation forFinset.sum (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y).
These support destructuring, for example ∑ ⟨x, y⟩ ∈ s ×ˢ t, f x y.
Notation: "∑" bigOpBinders* ("with" term)? "," term
Equations
- One or more equations did not get rendered due to their size.
Instances For
∏ x, f xis notation forFinset.prod Finset.univ f. It is the product off x, wherexranges over the finite domain off.∏ x ∈ s, f xis notation forFinset.prod s f. It is the product off x, wherexranges over the finite sets(either aFinsetor aSetwith aFintypeinstance).∏ x ∈ s with p x, f xis notation forFinset.prod (Finset.filter p s) f.∏ (x ∈ s) (y ∈ t), f x yis notation forFinset.prod (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y).
These support destructuring, for example ∏ ⟨x, y⟩ ∈ s ×ˢ t, f x y.
Notation: "∏" bigOpBinders* ("with" term)? "," term
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Deprecated, use ∑ x ∈ s, f x)
∑ x in s, f x is notation for Finset.sum s f. It is the sum of f x,
where x ranges over the finite set s.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Deprecated, use ∏ x ∈ s, f x)
∏ x in s, f x is notation for Finset.prod s f. It is the product of f x,
where x ranges over the finite set s.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Delaborator for Finset.prod. The pp.piBinderTypes option controls whether
to show the domain type when the product is over Finset.univ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Delaborator for Finset.sum. The pp.piBinderTypes option controls whether
to show the domain type when the sum is over Finset.univ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Finset.prod_eq_multiset_prod
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(s : Finset α)
(f : α → β)
:
∏ x ∈ s, f x = (Multiset.map f s.val).prod
theorem
Finset.sum_eq_multiset_sum
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset α)
(f : α → β)
:
∑ x ∈ s, f x = (Multiset.map f s.val).sum
@[simp]
theorem
Finset.prod_map_val
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(s : Finset α)
(f : α → β)
:
(Multiset.map f s.val).prod = ∏ a ∈ s, f a
@[simp]
theorem
Finset.sum_map_val
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset α)
(f : α → β)
:
(Multiset.map f s.val).sum = ∑ a ∈ s, f a
theorem
Finset.prod_eq_fold
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(s : Finset α)
(f : α → β)
:
∏ x ∈ s, f x = Finset.fold (fun (x1 x2 : β) => x1 * x2) 1 f s
theorem
Finset.sum_eq_fold
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset α)
(f : α → β)
:
∑ x ∈ s, f x = Finset.fold (fun (x1 x2 : β) => x1 + x2) 0 f s
@[simp]
@[simp]
theorem
map_prod
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[CommMonoid β]
[CommMonoid γ]
{G : Type u_6}
[FunLike G β γ]
[MonoidHomClass G β γ]
(g : G)
(f : α → β)
(s : Finset α)
:
g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)
@[simp]
theorem
map_sum
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddCommMonoid β]
[AddCommMonoid γ]
{G : Type u_6}
[FunLike G β γ]
[AddMonoidHomClass G β γ]
(g : G)
(f : α → β)
(s : Finset α)
:
g (∑ x ∈ s, f x) = ∑ x ∈ s, g (f x)
theorem
MonoidHom.coe_finset_prod
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[MulOneClass β]
[CommMonoid γ]
(f : α → β →* γ)
(s : Finset α)
:
⇑(∏ x ∈ s, f x) = ∏ x ∈ s, ⇑(f x)
theorem
AddMonoidHom.coe_finset_sum
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddZeroClass β]
[AddCommMonoid γ]
(f : α → β →+ γ)
(s : Finset α)
:
⇑(∑ x ∈ s, f x) = ∑ x ∈ s, ⇑(f x)
@[simp]
theorem
MonoidHom.finset_prod_apply
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[MulOneClass β]
[CommMonoid γ]
(f : α → β →* γ)
(s : Finset α)
(b : β)
:
(∏ x ∈ s, f x) b = ∏ x ∈ s, (f x) b
See also Finset.prod_apply, with the same conclusion but with the weaker hypothesis
f : α → β → γ
@[simp]
theorem
AddMonoidHom.finset_sum_apply
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddZeroClass β]
[AddCommMonoid γ]
(f : α → β →+ γ)
(s : Finset α)
(b : β)
:
(∑ x ∈ s, f x) b = ∑ x ∈ s, (f x) b
See also Finset.sum_apply, with the same conclusion but with the weaker hypothesis
f : α → β → γ
@[simp]
@[simp]
theorem
Finset.prod_of_isEmpty
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[CommMonoid β]
[IsEmpty α]
(s : Finset α)
:
∏ i ∈ s, f i = 1
theorem
Finset.sum_of_isEmpty
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[AddCommMonoid β]
[IsEmpty α]
(s : Finset α)
:
∑ i ∈ s, f i = 0
@[deprecated Finset.prod_of_isEmpty]
theorem
Finset.prod_of_empty
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[CommMonoid β]
[IsEmpty α]
(s : Finset α)
:
∏ i ∈ s, f i = 1
Alias of Finset.prod_of_isEmpty.
@[deprecated Finset.sum_of_isEmpty]
theorem
Finset.sum_of_empty
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[AddCommMonoid β]
[IsEmpty α]
(s : Finset α)
:
∑ i ∈ s, f i = 0
Alias of Finset.sum_of_isEmpty.
@[simp]
theorem
Finset.prod_cons
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{a : α}
{f : α → β}
[CommMonoid β]
(h : a ∉ s)
:
∏ x ∈ Finset.cons a s h, f x = f a * ∏ x ∈ s, f x
@[simp]
theorem
Finset.sum_cons
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{a : α}
{f : α → β}
[AddCommMonoid β]
(h : a ∉ s)
:
∑ x ∈ Finset.cons a s h, f x = f a + ∑ x ∈ s, f x
@[simp]
theorem
Finset.prod_insert
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{a : α}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
:
@[simp]
theorem
Finset.sum_insert
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{a : α}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
:
@[simp]
theorem
Finset.prod_insert_of_eq_one_if_not_mem
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{a : α}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
(h : a ∉ s → f a = 1)
:
The product of f over insert a s is the same as
the product over s, as long as a is in s or f a = 1.
@[simp]
theorem
Finset.sum_insert_of_eq_zero_if_not_mem
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{a : α}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
(h : a ∉ s → f a = 0)
:
The sum of f over insert a s is the same as
the sum over s, as long as a is in s or f a = 0.
@[simp]
theorem
Finset.prod_insert_one
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{a : α}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
(h : f a = 1)
:
The product of f over insert a s is the same as
the product over s, as long as f a = 1.
@[simp]
theorem
Finset.sum_insert_zero
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{a : α}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
(h : f a = 0)
:
The sum of f over insert a s is the same as
the sum over s, as long as f a = 0.
theorem
Finset.prod_insert_div
{α : Type u_3}
{s : Finset α}
{a : α}
{M : Type u_6}
[CommGroup M]
[DecidableEq α]
(ha : a ∉ s)
{f : α → M}
:
theorem
Finset.sum_insert_sub
{α : Type u_3}
{s : Finset α}
{a : α}
{M : Type u_6}
[AddCommGroup M]
[DecidableEq α]
(ha : a ∉ s)
{f : α → M}
:
@[simp]
theorem
Finset.prod_singleton
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(f : α → β)
(a : α)
:
∏ x ∈ {a}, f x = f a
@[simp]
theorem
Finset.sum_singleton
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(f : α → β)
(a : α)
:
∑ x ∈ {a}, f x = f a
theorem
Finset.prod_pair
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
{a b : α}
(h : a ≠ b)
:
theorem
Finset.sum_pair
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
{a b : α}
(h : a ≠ b)
:
@[simp]
theorem
Finset.prod_const_one
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[CommMonoid β]
:
∏ _x ∈ s, 1 = 1
@[simp]
theorem
Finset.sum_const_zero
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[AddCommMonoid β]
:
∑ _x ∈ s, 0 = 0
@[simp]
theorem
Finset.prod_image
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
{s : Finset γ}
{g : γ → α}
:
(∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) → ∏ x ∈ Finset.image g s, f x = ∏ x ∈ s, f (g x)
@[simp]
theorem
Finset.sum_image
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset γ}
{g : γ → α}
:
(∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) → ∑ x ∈ Finset.image g s, f x = ∑ x ∈ s, f (g x)
@[simp]
theorem
Finset.prod_map
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[CommMonoid β]
(s : Finset α)
(e : α ↪ γ)
(f : γ → β)
:
∏ x ∈ Finset.map e s, f x = ∏ x ∈ s, f (e x)
@[simp]
theorem
Finset.sum_map
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddCommMonoid β]
(s : Finset α)
(e : α ↪ γ)
(f : γ → β)
:
∑ x ∈ Finset.map e s, f x = ∑ x ∈ s, f (e x)
theorem
Finset.prod_attach
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(s : Finset α)
(f : α → β)
:
∏ x ∈ s.attach, f ↑x = ∏ x ∈ s, f x
theorem
Finset.sum_attach
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset α)
(f : α → β)
:
∑ x ∈ s.attach, f ↑x = ∑ x ∈ s, f x
theorem
Finset.prod_congr
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f g : α → β}
[CommMonoid β]
(h : s₁ = s₂)
:
theorem
Finset.sum_congr
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f g : α → β}
[AddCommMonoid β]
(h : s₁ = s₂)
:
theorem
Finset.prod_eq_one
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
{f : α → β}
{s : Finset α}
(h : ∀ x ∈ s, f x = 1)
:
∏ x ∈ s, f x = 1
theorem
Finset.sum_eq_zero
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
{f : α → β}
{s : Finset α}
(h : ∀ x ∈ s, f x = 0)
:
∑ x ∈ s, f x = 0
theorem
Finset.prod_disjUnion
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[CommMonoid β]
(h : Disjoint s₁ s₂)
:
theorem
Finset.sum_disjUnion
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[AddCommMonoid β]
(h : Disjoint s₁ s₂)
:
theorem
Finset.prod_disjiUnion
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[CommMonoid β]
(s : Finset ι)
(t : ι → Finset α)
(h : (↑s).PairwiseDisjoint t)
:
∏ x ∈ s.disjiUnion t h, f x = ∏ i ∈ s, ∏ x ∈ t i, f x
theorem
Finset.sum_disjiUnion
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[AddCommMonoid β]
(s : Finset ι)
(t : ι → Finset α)
(h : (↑s).PairwiseDisjoint t)
:
∑ x ∈ s.disjiUnion t h, f x = ∑ i ∈ s, ∑ x ∈ t i, f x
theorem
Finset.prod_union_inter
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
:
theorem
Finset.sum_union_inter
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
:
theorem
Finset.prod_union
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
(h : Disjoint s₁ s₂)
:
theorem
Finset.sum_union
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
(h : Disjoint s₁ s₂)
:
theorem
Finset.prod_filter_mul_prod_filter_not
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(s : Finset α)
(p : α → Prop)
[DecidablePred p]
[(x : α) → Decidable ¬p x]
(f : α → β)
:
(∏ x ∈ Finset.filter (fun (x : α) => p x) s, f x) * ∏ x ∈ Finset.filter (fun (x : α) => ¬p x) s, f x = ∏ x ∈ s, f x
theorem
Finset.sum_filter_add_sum_filter_not
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset α)
(p : α → Prop)
[DecidablePred p]
[(x : α) → Decidable ¬p x]
(f : α → β)
:
∑ x ∈ Finset.filter (fun (x : α) => p x) s, f x + ∑ x ∈ Finset.filter (fun (x : α) => ¬p x) s, f x = ∑ x ∈ s, f x
theorem
Finset.prod_filter_not_mul_prod_filter
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(s : Finset α)
(p : α → Prop)
[DecidablePred p]
[(x : α) → Decidable ¬p x]
(f : α → β)
:
(∏ x ∈ Finset.filter (fun (x : α) => ¬p x) s, f x) * ∏ x ∈ Finset.filter p s, f x = ∏ x ∈ s, f x
theorem
Finset.sum_filter_not_add_sum_filter
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset α)
(p : α → Prop)
[DecidablePred p]
[(x : α) → Decidable ¬p x]
(f : α → β)
:
∑ x ∈ Finset.filter (fun (x : α) => ¬p x) s, f x + ∑ x ∈ Finset.filter p s, f x = ∑ x ∈ s, f x
theorem
Finset.prod_filter_xor
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommMonoid β]
(p q : α → Prop)
[DecidablePred p]
[DecidablePred q]
:
∏ x ∈ Finset.filter (fun (x : α) => Xor' (p x) (q x)) s, f x = (∏ x ∈ Finset.filter (fun (x : α) => p x ∧ ¬q x) s, f x) * ∏ x ∈ Finset.filter (fun (x : α) => q x ∧ ¬p x) s, f x
theorem
Finset.sum_filter_xor
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
(p q : α → Prop)
[DecidablePred p]
[DecidablePred q]
:
∑ x ∈ Finset.filter (fun (x : α) => Xor' (p x) (q x)) s, f x = ∑ x ∈ Finset.filter (fun (x : α) => p x ∧ ¬q x) s, f x + ∑ x ∈ Finset.filter (fun (x : α) => q x ∧ ¬p x) s, f x
@[simp]
theorem
Finset.prod_to_list
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(s : Finset α)
(f : α → β)
:
@[simp]
theorem
Finset.sum_to_list
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset α)
(f : α → β)
:
theorem
Equiv.Perm.prod_comp
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(σ : Equiv.Perm α)
(s : Finset α)
(f : α → β)
(hs : {a : α | σ a ≠ a} ⊆ ↑s)
:
∏ x ∈ s, f (σ x) = ∏ x ∈ s, f x
theorem
Equiv.Perm.sum_comp
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(σ : Equiv.Perm α)
(s : Finset α)
(f : α → β)
(hs : {a : α | σ a ≠ a} ⊆ ↑s)
:
∑ x ∈ s, f (σ x) = ∑ x ∈ s, f x
theorem
Equiv.Perm.prod_comp'
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(σ : Equiv.Perm α)
(s : Finset α)
(f : α → α → β)
(hs : {a : α | σ a ≠ a} ⊆ ↑s)
:
∏ x ∈ s, f (σ x) x = ∏ x ∈ s, f x ((Equiv.symm σ) x)
theorem
Equiv.Perm.sum_comp'
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(σ : Equiv.Perm α)
(s : Finset α)
(f : α → α → β)
(hs : {a : α | σ a ≠ a} ⊆ ↑s)
:
∑ x ∈ s, f (σ x) x = ∑ x ∈ s, f x ((Equiv.symm σ) x)
theorem
Finset.prod_powerset_insert
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{a : α}
[CommMonoid β]
[DecidableEq α]
(ha : a ∉ s)
(f : Finset α → β)
:
A product over all subsets of s ∪ {x} is obtained by multiplying the product over all subsets
of s, and over all subsets of s to which one adds x.
theorem
Finset.sum_powerset_insert
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{a : α}
[AddCommMonoid β]
[DecidableEq α]
(ha : a ∉ s)
(f : Finset α → β)
:
A sum over all subsets of s ∪ {x} is obtained by summing the sum over all subsets
of s, and over all subsets of s to which one adds x.
theorem
Finset.prod_powerset_cons
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{a : α}
[CommMonoid β]
(ha : a ∉ s)
(f : Finset α → β)
:
∏ t ∈ (Finset.cons a s ha).powerset, f t = (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset.attach, f (Finset.cons a ↑t ⋯)
A product over all subsets of s ∪ {x} is obtained by multiplying the product over all subsets
of s, and over all subsets of s to which one adds x.
theorem
Finset.sum_powerset_cons
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{a : α}
[AddCommMonoid β]
(ha : a ∉ s)
(f : Finset α → β)
:
∑ t ∈ (Finset.cons a s ha).powerset, f t = ∑ t ∈ s.powerset, f t + ∑ t ∈ s.powerset.attach, f (Finset.cons a ↑t ⋯)
A sum over all subsets of s ∪ {x} is obtained by summing the sum over all subsets
of s, and over all subsets of s to which one adds x.
theorem
Finset.prod_powerset
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(s : Finset α)
(f : Finset α → β)
:
∏ t ∈ s.powerset, f t = ∏ j ∈ Finset.range (s.card + 1), ∏ t ∈ Finset.powersetCard j s, f t
A product over powerset s is equal to the double product over sets of subsets of s with
#s = k, for k = 1, ..., #s.
theorem
Finset.sum_powerset
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset α)
(f : Finset α → β)
:
∑ t ∈ s.powerset, f t = ∑ j ∈ Finset.range (s.card + 1), ∑ t ∈ Finset.powersetCard j s, f t
A sum over powerset s is equal to the double sum over sets of subsets of s with
#s = k, for k = 1, ..., #s
theorem
IsCompl.prod_mul_prod
{α : Type u_3}
{β : Type u_4}
[Fintype α]
[CommMonoid β]
{s t : Finset α}
(h : IsCompl s t)
(f : α → β)
:
theorem
IsCompl.sum_add_sum
{α : Type u_3}
{β : Type u_4}
[Fintype α]
[AddCommMonoid β]
{s t : Finset α}
(h : IsCompl s t)
(f : α → β)
:
theorem
Finset.prod_mul_prod_compl
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[Fintype α]
[DecidableEq α]
(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.sum_add_sum_compl
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[Fintype α]
[DecidableEq α]
(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_compl_mul_prod
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[Fintype α]
[DecidableEq α]
(s : Finset α)
(f : α → β)
:
theorem
Finset.sum_compl_add_sum
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[Fintype α]
[DecidableEq α]
(s : Finset α)
(f : α → β)
:
theorem
Finset.prod_sdiff
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
(h : s₁ ⊆ s₂)
:
theorem
Finset.sum_sdiff
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
(h : s₁ ⊆ s₂)
:
theorem
Finset.prod_subset_one_on_sdiff
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f g : α → β}
[CommMonoid β]
[DecidableEq α]
(h : s₁ ⊆ s₂)
(hg : ∀ x ∈ s₂ \ s₁, g x = 1)
(hfg : ∀ x ∈ s₁, f x = g x)
:
∏ i ∈ s₁, f i = ∏ i ∈ s₂, g i
theorem
Finset.sum_subset_zero_on_sdiff
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f g : α → β}
[AddCommMonoid β]
[DecidableEq α]
(h : s₁ ⊆ s₂)
(hg : ∀ x ∈ s₂ \ s₁, g x = 0)
(hfg : ∀ x ∈ s₁, f x = g x)
:
∑ i ∈ s₁, f i = ∑ i ∈ s₂, g i
theorem
Finset.prod_subset
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[CommMonoid β]
(h : s₁ ⊆ s₂)
(hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 1)
:
∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x
theorem
Finset.sum_subset
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[AddCommMonoid β]
(h : s₁ ⊆ s₂)
(hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 0)
:
∑ x ∈ s₁, f x = ∑ x ∈ s₂, f x
theorem
Finset.prod_biUnion
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
{s : Finset γ}
{t : γ → Finset α}
(hs : (↑s).PairwiseDisjoint t)
:
∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i
theorem
Finset.sum_biUnion
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset γ}
{t : γ → Finset α}
(hs : (↑s).PairwiseDisjoint t)
:
∑ x ∈ s.biUnion t, f x = ∑ x ∈ s, ∑ i ∈ t x, f i
theorem
Finset.prod_sigma
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
{σ : α → Type u_6}
(s : Finset α)
(t : (a : α) → Finset (σ a))
(f : Sigma σ → β)
:
∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩
The product over a sigma type equals the product of the fiberwise products. For rewriting
in the reverse direction, use Finset.prod_sigma'.
theorem
Finset.sum_sigma
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
{σ : α → Type u_6}
(s : Finset α)
(t : (a : α) → Finset (σ a))
(f : Sigma σ → β)
:
∑ x ∈ s.sigma t, f x = ∑ a ∈ s, ∑ s ∈ t a, f ⟨a, s⟩
The sum over a sigma type equals the sum of the fiberwise sums. For rewriting
in the reverse direction, use Finset.sum_sigma'
theorem
Finset.prod_sigma'
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
{σ : α → Type u_6}
(s : Finset α)
(t : (a : α) → Finset (σ a))
(f : (a : α) → σ a → β)
:
∏ a ∈ s, ∏ s ∈ t a, f a s = ∏ x ∈ s.sigma t, f x.fst x.snd
The product over a sigma type equals the product of the fiberwise products. For rewriting
in the reverse direction, use Finset.prod_sigma.
theorem
Finset.sum_sigma'
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
{σ : α → Type u_6}
(s : Finset α)
(t : (a : α) → Finset (σ a))
(f : (a : α) → σ a → β)
:
∑ a ∈ s, ∑ s ∈ t a, f a s = ∑ x ∈ s.sigma t, f x.fst x.snd
The sum over a sigma type equals the sum of the fiberwise sums. For rewriting
in the reverse direction, use Finset.sum_sigma
theorem
Finset.prod_bij
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
{s : Finset ι}
{t : Finset κ}
{f : ι → α}
{g : κ → α}
(i : (a : ι) → a ∈ s → κ)
(hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t)
(i_inj : ∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
(i_surj : ∀ b ∈ t, ∃ (a : ι) (ha : a ∈ s), i a ha = b)
(h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha))
:
∏ x ∈ s, f x = ∏ x ∈ t, g x
Reorder a product.
The difference with Finset.prod_bij' is that the bijection is specified as a surjective injection,
rather than by an inverse function.
The difference with Finset.prod_nbij is that the bijection is allowed to use membership of the
domain of the product, rather than being a non-dependent function.
theorem
Finset.sum_bij
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
{s : Finset ι}
{t : Finset κ}
{f : ι → α}
{g : κ → α}
(i : (a : ι) → a ∈ s → κ)
(hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t)
(i_inj : ∀ (a₁ : ι) (ha₁ : a₁ ∈ s) (a₂ : ι) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
(i_surj : ∀ b ∈ t, ∃ (a : ι) (ha : a ∈ s), i a ha = b)
(h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha))
:
∑ x ∈ s, f x = ∑ x ∈ t, g x
Reorder a sum.
The difference with Finset.sum_bij' is that the bijection is specified as a surjective injection,
rather than by an inverse function.
The difference with Finset.sum_nbij is that the bijection is allowed to use membership of the
domain of the sum, rather than being a non-dependent function.
theorem
Finset.prod_bij'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
{s : Finset ι}
{t : Finset κ}
{f : ι → α}
{g : κ → α}
(i : (a : ι) → a ∈ s → κ)
(j : (a : κ) → a ∈ t → ι)
(hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ 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)
(h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha))
:
∏ x ∈ s, f x = ∏ x ∈ t, g x
Reorder a product.
The difference with Finset.prod_bij is that the bijection is specified with an inverse, rather
than as a surjective injection.
The difference with Finset.prod_nbij' is that the bijection and its inverse are allowed to use
membership of the domains of the products, rather than being non-dependent functions.
theorem
Finset.sum_bij'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
{s : Finset ι}
{t : Finset κ}
{f : ι → α}
{g : κ → α}
(i : (a : ι) → a ∈ s → κ)
(j : (a : κ) → a ∈ t → ι)
(hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ 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)
(h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha))
:
∑ x ∈ s, f x = ∑ x ∈ t, g x
Reorder a sum.
The difference with Finset.sum_bij is that the bijection is specified with an inverse, rather than
as a surjective injection.
The difference with Finset.sum_nbij' is that the bijection and its inverse are allowed to use
membership of the domains of the sums, rather than being non-dependent functions.
theorem
Finset.prod_nbij
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
{s : Finset ι}
{t : Finset κ}
{f : ι → α}
{g : κ → α}
(i : ι → κ)
(hi : ∀ a ∈ s, i a ∈ t)
(i_inj : Set.InjOn i ↑s)
(i_surj : Set.SurjOn i ↑s ↑t)
(h : ∀ a ∈ s, f a = g (i a))
:
∏ x ∈ s, f x = ∏ x ∈ t, g x
Reorder a product.
The difference with Finset.prod_nbij' is that the bijection is specified as a surjective
injection, rather than by an inverse function.
The difference with Finset.prod_bij is that the bijection is a non-dependent function, rather than
being allowed to use membership of the domain of the product.
theorem
Finset.sum_nbij
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
{s : Finset ι}
{t : Finset κ}
{f : ι → α}
{g : κ → α}
(i : ι → κ)
(hi : ∀ a ∈ s, i a ∈ t)
(i_inj : Set.InjOn i ↑s)
(i_surj : Set.SurjOn i ↑s ↑t)
(h : ∀ a ∈ s, f a = g (i a))
:
∑ x ∈ s, f x = ∑ x ∈ t, g x
Reorder a sum.
The difference with Finset.sum_nbij' is that the bijection is specified as a surjective injection,
rather than by an inverse function.
The difference with Finset.sum_bij is that the bijection is a non-dependent function, rather than
being allowed to use membership of the domain of the sum.
theorem
Finset.prod_nbij'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
{s : Finset ι}
{t : Finset κ}
{f : ι → α}
{g : κ → α}
(i : ι → κ)
(j : κ → ι)
(hi : ∀ a ∈ s, i a ∈ t)
(hj : ∀ a ∈ t, j a ∈ s)
(left_inv : ∀ a ∈ s, j (i a) = a)
(right_inv : ∀ a ∈ t, i (j a) = a)
(h : ∀ a ∈ s, f a = g (i a))
:
∏ x ∈ s, f x = ∏ x ∈ t, g x
Reorder a product.
The difference with Finset.prod_nbij is that the bijection is specified with an inverse, rather
than as a surjective injection.
The difference with Finset.prod_bij' is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains of the products.
The difference with Finset.prod_equiv is that bijectivity is only required to hold on the domains
of the products, rather than on the entire types.
theorem
Finset.sum_nbij'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
{s : Finset ι}
{t : Finset κ}
{f : ι → α}
{g : κ → α}
(i : ι → κ)
(j : κ → ι)
(hi : ∀ a ∈ s, i a ∈ t)
(hj : ∀ a ∈ t, j a ∈ s)
(left_inv : ∀ a ∈ s, j (i a) = a)
(right_inv : ∀ a ∈ t, i (j a) = a)
(h : ∀ a ∈ s, f a = g (i a))
:
∑ x ∈ s, f x = ∑ x ∈ t, g x
Reorder a sum.
The difference with Finset.sum_nbij is that the bijection is specified with an inverse, rather
than as a surjective injection.
The difference with Finset.sum_bij' is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains of the sums.
The difference with Finset.sum_equiv is that bijectivity is only required to hold on the domains
of the sums, rather than on the entire types.
theorem
Finset.prod_equiv
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
{s : Finset ι}
{t : Finset κ}
{f : ι → α}
{g : κ → α}
(e : ι ≃ κ)
(hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t)
(hfg : ∀ i ∈ s, f i = g (e i))
:
∏ i ∈ s, f i = ∏ i ∈ t, g i
Specialization of Finset.prod_nbij' that automatically fills in most arguments.
See Fintype.prod_equiv for the version where s and t are univ.
theorem
Finset.sum_equiv
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
{s : Finset ι}
{t : Finset κ}
{f : ι → α}
{g : κ → α}
(e : ι ≃ κ)
(hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t)
(hfg : ∀ i ∈ s, f i = g (e i))
:
∑ i ∈ s, f i = ∑ i ∈ t, g i
Specialization of Finset.sum_nbij'` that automatically fills in most arguments.
See Fintype.sum_equiv for the version where s and t are univ.
theorem
Finset.prod_bijective
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
{s : Finset ι}
{t : Finset κ}
{f : ι → α}
{g : κ → α}
(e : ι → κ)
(he : Function.Bijective e)
(hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t)
(hfg : ∀ i ∈ s, f i = g (e i))
:
∏ i ∈ s, f i = ∏ i ∈ t, g i
Specialization of Finset.prod_bij that automatically fills in most arguments.
See Fintype.prod_bijective for the version where s and t are univ.
theorem
Finset.sum_bijective
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
{s : Finset ι}
{t : Finset κ}
{f : ι → α}
{g : κ → α}
(e : ι → κ)
(he : Function.Bijective e)
(hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t)
(hfg : ∀ i ∈ s, f i = g (e i))
:
∑ i ∈ s, f i = ∑ i ∈ t, g i
Specialization of Finset.sum_bij` that automatically fills in most arguments.
See Fintype.sum_bijective for the version where s and t are univ.
theorem
Finset.prod_of_injOn
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
{s : Finset ι}
{t : Finset κ}
{f : ι → α}
{g : κ → α}
(e : ι → κ)
(he : Set.InjOn e ↑s)
(hest : Set.MapsTo e ↑s ↑t)
(h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1)
(h : ∀ i ∈ s, f i = g (e i))
:
∏ i ∈ s, f i = ∏ j ∈ t, g j
theorem
Finset.sum_of_injOn
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
{s : Finset ι}
{t : Finset κ}
{f : ι → α}
{g : κ → α}
(e : ι → κ)
(he : Set.InjOn e ↑s)
(hest : Set.MapsTo e ↑s ↑t)
(h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 0)
(h : ∀ i ∈ s, f i = g (e i))
:
∑ i ∈ s, f i = ∑ j ∈ t, g j
theorem
Finset.prod_fiberwise_eq_prod_filter
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
[DecidableEq κ]
(s : Finset ι)
(t : Finset κ)
(g : ι → κ)
(f : ι → α)
:
∏ j ∈ t, ∏ i ∈ Finset.filter (fun (i : ι) => g i = j) s, f i = ∏ i ∈ Finset.filter (fun (i : ι) => g i ∈ t) s, f i
theorem
Finset.sum_fiberwise_eq_sum_filter
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
[DecidableEq κ]
(s : Finset ι)
(t : Finset κ)
(g : ι → κ)
(f : ι → α)
:
∑ j ∈ t, ∑ i ∈ Finset.filter (fun (i : ι) => g i = j) s, f i = ∑ i ∈ Finset.filter (fun (i : ι) => g i ∈ t) s, f i
theorem
Finset.prod_fiberwise_eq_prod_filter'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
[DecidableEq κ]
(s : Finset ι)
(t : Finset κ)
(g : ι → κ)
(f : κ → α)
:
∏ j ∈ t, ∏ i ∈ Finset.filter (fun (i : ι) => g i = j) s, f j = ∏ i ∈ Finset.filter (fun (i : ι) => g i ∈ t) s, f (g i)
theorem
Finset.sum_fiberwise_eq_sum_filter'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
[DecidableEq κ]
(s : Finset ι)
(t : Finset κ)
(g : ι → κ)
(f : κ → α)
:
∑ j ∈ t, ∑ i ∈ Finset.filter (fun (i : ι) => g i = j) s, f j = ∑ i ∈ Finset.filter (fun (i : ι) => g i ∈ t) s, f (g i)
theorem
Finset.prod_fiberwise_of_maps_to
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
{s : Finset ι}
{t : Finset κ}
[DecidableEq κ]
{g : ι → κ}
(h : ∀ i ∈ s, g i ∈ t)
(f : ι → α)
:
∏ j ∈ t, ∏ i ∈ Finset.filter (fun (i : ι) => g i = j) s, f i = ∏ i ∈ s, f i
theorem
Finset.sum_fiberwise_of_maps_to
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
{s : Finset ι}
{t : Finset κ}
[DecidableEq κ]
{g : ι → κ}
(h : ∀ i ∈ s, g i ∈ t)
(f : ι → α)
:
∑ j ∈ t, ∑ i ∈ Finset.filter (fun (i : ι) => g i = j) s, f i = ∑ i ∈ s, f i
theorem
Finset.prod_fiberwise_of_maps_to'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
{s : Finset ι}
{t : Finset κ}
[DecidableEq κ]
{g : ι → κ}
(h : ∀ i ∈ s, g i ∈ t)
(f : κ → α)
:
∏ j ∈ t, ∏ i ∈ Finset.filter (fun (i : ι) => g i = j) s, f j = ∏ i ∈ s, f (g i)
theorem
Finset.sum_fiberwise_of_maps_to'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
{s : Finset ι}
{t : Finset κ}
[DecidableEq κ]
{g : ι → κ}
(h : ∀ i ∈ s, g i ∈ t)
(f : κ → α)
:
∑ j ∈ t, ∑ i ∈ Finset.filter (fun (i : ι) => g i = j) s, f j = ∑ i ∈ s, f (g i)
theorem
Finset.prod_fiberwise
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
[DecidableEq κ]
[Fintype κ]
(s : Finset ι)
(g : ι → κ)
(f : ι → α)
:
∏ j : κ, ∏ i ∈ Finset.filter (fun (i : ι) => g i = j) s, f i = ∏ i ∈ s, f i
theorem
Finset.sum_fiberwise
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
[DecidableEq κ]
[Fintype κ]
(s : Finset ι)
(g : ι → κ)
(f : ι → α)
:
∑ j : κ, ∑ i ∈ Finset.filter (fun (i : ι) => g i = j) s, f i = ∑ i ∈ s, f i
theorem
Finset.prod_fiberwise'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
[DecidableEq κ]
[Fintype κ]
(s : Finset ι)
(g : ι → κ)
(f : κ → α)
:
∏ j : κ, ∏ i ∈ Finset.filter (fun (i : ι) => g i = j) s, f j = ∏ i ∈ s, f (g i)
theorem
Finset.sum_fiberwise'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
[DecidableEq κ]
[Fintype κ]
(s : Finset ι)
(g : ι → κ)
(f : κ → α)
:
∑ j : κ, ∑ i ∈ Finset.filter (fun (i : ι) => g i = j) s, f j = ∑ i ∈ s, f (g i)
theorem
Finset.prod_univ_pi
{ι : Type u_1}
{β : Type u_4}
[CommMonoid β]
[DecidableEq ι]
[Fintype ι]
{κ : ι → Type u_6}
(t : (i : ι) → Finset (κ i))
(f : ((i : ι) → i ∈ Finset.univ → κ i) → β)
:
∏ x ∈ Finset.univ.pi t, f x = ∏ x ∈ Fintype.piFinset t, f fun (a : ι) (x_1 : a ∈ Finset.univ) => x a
Taking a product over univ.pi t is the same as taking the product over Fintype.piFinset t.
univ.pi t and Fintype.piFinset t are essentially the same Finset, but differ
in the type of their element, univ.pi t is a Finset (Π a ∈ univ, t a) and
Fintype.piFinset t is a Finset (Π a, t a).
theorem
Finset.sum_univ_pi
{ι : Type u_1}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq ι]
[Fintype ι]
{κ : ι → Type u_6}
(t : (i : ι) → Finset (κ i))
(f : ((i : ι) → i ∈ Finset.univ → κ i) → β)
:
∑ x ∈ Finset.univ.pi t, f x = ∑ x ∈ Fintype.piFinset t, f fun (a : ι) (x_1 : a ∈ Finset.univ) => x a
Taking a sum over univ.pi t is the same as taking the sum over
Fintype.piFinset t. univ.pi t and Fintype.piFinset t are essentially the same Finset,
but differ in the type of their element, univ.pi t is a Finset (Π a ∈ univ, t a) and
Fintype.piFinset t is a Finset (Π a, t a).
@[simp]
theorem
Finset.prod_diag
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α × α → β)
:
∏ i ∈ s.diag, f i = ∏ i ∈ s, f (i, i)
@[simp]
theorem
Finset.sum_diag
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α × α → β)
:
∑ i ∈ s.diag, f i = ∑ i ∈ s, f (i, i)
theorem
Finset.prod_image'
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
{s : Finset ι}
{g : ι → α}
(h : ι → β)
(eq : ∀ i ∈ s, f (g i) = ∏ j ∈ Finset.filter (fun (j : ι) => g j = g i) s, h j)
:
∏ a ∈ Finset.image g s, f a = ∏ i ∈ s, h i
theorem
Finset.sum_image'
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset ι}
{g : ι → α}
(h : ι → β)
(eq : ∀ i ∈ s, f (g i) = ∑ j ∈ Finset.filter (fun (j : ι) => g j = g i) s, h j)
:
∑ a ∈ Finset.image g s, f a = ∑ i ∈ s, h i
theorem
Finset.prod_mul_distrib
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f g : α → β}
[CommMonoid β]
:
theorem
Finset.sum_add_distrib
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f g : α → β}
[AddCommMonoid β]
:
theorem
Finset.prod_product
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[CommMonoid β]
(s : Finset γ)
(t : Finset α)
(f : γ × α → β)
:
The product over a product set equals the product of the fiberwise products. For rewriting
in the reverse direction, use Finset.prod_product'.
theorem
Finset.sum_product
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddCommMonoid β]
(s : Finset γ)
(t : Finset α)
(f : γ × α → β)
:
The sum over a product set equals the sum of the fiberwise sums. For rewriting
in the reverse direction, use Finset.sum_product'
theorem
Finset.prod_product'
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[CommMonoid β]
(s : Finset γ)
(t : Finset α)
(f : γ → α → β)
:
The product over a product set equals the product of the fiberwise products. For rewriting
in the reverse direction, use Finset.prod_product.
theorem
Finset.sum_product'
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddCommMonoid β]
(s : Finset γ)
(t : Finset α)
(f : γ → α → β)
:
The sum over a product set equals the sum of the fiberwise sums. For rewriting
in the reverse direction, use Finset.sum_product
theorem
Finset.prod_product_right'
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[CommMonoid β]
(s : Finset γ)
(t : Finset α)
(f : γ → α → β)
:
An uncurried version of Finset.prod_product_right.
theorem
Finset.sum_product_right'
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddCommMonoid β]
(s : Finset γ)
(t : Finset α)
(f : γ → α → β)
:
An uncurried version of Finset.sum_product_right
theorem
Finset.prod_comm'
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[CommMonoid β]
{s : Finset γ}
{t : γ → Finset α}
{t' : Finset α}
{s' : α → Finset γ}
(h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t')
{f : γ → α → β}
:
∏ x ∈ s, ∏ y ∈ t x, f x y = ∏ y ∈ t', ∏ x ∈ s' y, f x y
Generalization of Finset.prod_comm to the case when the inner Finsets depend on the outer
variable.
theorem
Finset.sum_comm'
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddCommMonoid β]
{s : Finset γ}
{t : γ → Finset α}
{t' : Finset α}
{s' : α → Finset γ}
(h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t')
{f : γ → α → β}
:
∑ x ∈ s, ∑ y ∈ t x, f x y = ∑ y ∈ t', ∑ x ∈ s' y, f x y
Generalization of Finset.sum_comm to the case when the inner Finsets depend on
the outer variable.
theorem
Finset.prod_comm
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[CommMonoid β]
{s : Finset γ}
{t : Finset α}
{f : γ → α → β}
:
∏ x ∈ s, ∏ y ∈ t, f x y = ∏ y ∈ t, ∏ x ∈ s, f x y
theorem
Finset.sum_comm
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddCommMonoid β]
{s : Finset γ}
{t : Finset α}
{f : γ → α → β}
:
∑ x ∈ s, ∑ y ∈ t, f x y = ∑ y ∈ t, ∑ x ∈ s, f x y
theorem
Finset.prod_hom_rel
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[CommMonoid β]
[CommMonoid γ]
{r : β → γ → Prop}
{f : α → β}
{g : α → γ}
{s : Finset α}
(h₁ : r 1 1)
(h₂ : ∀ (a : α) (b : β) (c : γ), r b c → r (f a * b) (g a * c))
:
r (∏ x ∈ s, f x) (∏ x ∈ s, g x)
theorem
Finset.sum_hom_rel
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddCommMonoid β]
[AddCommMonoid γ]
{r : β → γ → Prop}
{f : α → β}
{g : α → γ}
{s : Finset α}
(h₁ : r 0 0)
(h₂ : ∀ (a : α) (b : β) (c : γ), r b c → r (f a + b) (g a + c))
:
r (∑ x ∈ s, f x) (∑ x ∈ s, g x)
theorem
Finset.prod_filter_of_ne
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommMonoid β]
{p : α → Prop}
[DecidablePred p]
(hp : ∀ x ∈ s, f x ≠ 1 → p x)
:
∏ x ∈ Finset.filter (fun (x : α) => p x) s, f x = ∏ x ∈ s, f x
theorem
Finset.sum_filter_of_ne
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
{p : α → Prop}
[DecidablePred p]
(hp : ∀ x ∈ s, f x ≠ 0 → p x)
:
∑ x ∈ Finset.filter (fun (x : α) => p x) s, f x = ∑ x ∈ s, f x
theorem
Finset.prod_filter_ne_one
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[CommMonoid β]
(s : Finset α)
[(x : α) → Decidable (f x ≠ 1)]
:
∏ x ∈ Finset.filter (fun (x : α) => f x ≠ 1) s, f x = ∏ x ∈ s, f x
theorem
Finset.sum_filter_ne_zero
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[AddCommMonoid β]
(s : Finset α)
[(x : α) → Decidable (f x ≠ 0)]
:
∑ x ∈ Finset.filter (fun (x : α) => f x ≠ 0) s, f x = ∑ x ∈ s, f x
theorem
Finset.prod_filter
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[CommMonoid β]
(p : α → Prop)
[DecidablePred p]
(f : α → β)
:
∏ a ∈ Finset.filter (fun (a : α) => p a) s, f a = ∏ a ∈ s, if p a then f a else 1
theorem
Finset.sum_filter
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[AddCommMonoid β]
(p : α → Prop)
[DecidablePred p]
(f : α → β)
:
∑ a ∈ Finset.filter (fun (a : α) => p a) s, f a = ∑ a ∈ s, if p a then f a else 0
theorem
Finset.prod_eq_single_of_mem
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
{s : Finset α}
{f : α → β}
(a : α)
(h : a ∈ s)
(h₀ : ∀ b ∈ s, b ≠ a → f b = 1)
:
∏ x ∈ s, f x = f a
theorem
Finset.sum_eq_single_of_mem
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
{s : Finset α}
{f : α → β}
(a : α)
(h : a ∈ s)
(h₀ : ∀ b ∈ s, b ≠ a → f b = 0)
:
∑ x ∈ s, f x = f a
theorem
Finset.prod_eq_single
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
{s : Finset α}
{f : α → β}
(a : α)
(h₀ : ∀ b ∈ s, b ≠ a → f b = 1)
(h₁ : a ∉ s → f a = 1)
:
∏ x ∈ s, f x = f a
theorem
Finset.sum_eq_single
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
{s : Finset α}
{f : α → β}
(a : α)
(h₀ : ∀ b ∈ s, b ≠ a → f b = 0)
(h₁ : a ∉ s → f a = 0)
:
∑ x ∈ s, f x = f a
theorem
Finset.prod_union_eq_left
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
(hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 1)
:
theorem
Finset.sum_union_eq_left
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
(hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 0)
:
theorem
Finset.prod_union_eq_right
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
(hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1)
:
theorem
Finset.sum_union_eq_right
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
(hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 0)
:
@[simp]
theorem
Finset.prod_subtype_eq_prod_filter
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[CommMonoid β]
(f : α → β)
{p : α → Prop}
[DecidablePred p]
:
∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ Finset.filter (fun (x : α) => p x) s, f x
A product over s.subtype p equals one over {x ∈ s | p x}.
@[simp]
theorem
Finset.sum_subtype_eq_sum_filter
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[AddCommMonoid β]
(f : α → β)
{p : α → Prop}
[DecidablePred p]
:
∑ x ∈ Finset.subtype p s, f ↑x = ∑ x ∈ Finset.filter (fun (x : α) => p x) s, f x
A sum over s.subtype p equals one over {x ∈ s | p x}.
theorem
Finset.prod_subtype_of_mem
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[CommMonoid β]
(f : α → β)
{p : α → Prop}
[DecidablePred p]
(h : ∀ x ∈ s, p x)
:
∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s, f x
If all elements of a Finset satisfy the predicate p, a product
over s.subtype p equals that product over s.
theorem
Finset.sum_subtype_of_mem
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[AddCommMonoid β]
(f : α → β)
{p : α → Prop}
[DecidablePred p]
(h : ∀ x ∈ s, p x)
:
∑ x ∈ Finset.subtype p s, f ↑x = ∑ x ∈ s, f x
If all elements of a Finset satisfy the predicate p, a sum
over s.subtype p equals that sum over s.
theorem
Finset.prod_subtype_map_embedding
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
{p : α → Prop}
{s : Finset { x : α // p x }}
{f : { x : α // p x } → β}
{g : α → β}
(h : ∀ x ∈ s, g ↑x = f x)
:
∏ x ∈ Finset.map (Function.Embedding.subtype fun (x : α) => p x) s, g x = ∏ x ∈ s, f x
A product of a function over a Finset in a subtype equals a
product in the main type of a function that agrees with the first
function on that Finset.
theorem
Finset.sum_subtype_map_embedding
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
{p : α → Prop}
{s : Finset { x : α // p x }}
{f : { x : α // p x } → β}
{g : α → β}
(h : ∀ x ∈ s, g ↑x = f x)
:
∑ x ∈ Finset.map (Function.Embedding.subtype fun (x : α) => p x) s, g x = ∑ x ∈ s, f x
A sum of a function over a Finset in a subtype equals a
sum in the main type of a function that agrees with the first
function on that Finset.
theorem
Finset.prod_coe_sort_eq_attach
{α : Type u_3}
{β : Type u_4}
(s : Finset α)
[CommMonoid β]
(f : { x : α // x ∈ s } → β)
:
theorem
Finset.sum_coe_sort_eq_attach
{α : Type u_3}
{β : Type u_4}
(s : Finset α)
[AddCommMonoid β]
(f : { x : α // x ∈ s } → β)
:
theorem
Finset.prod_coe_sort
{α : Type u_3}
{β : Type u_4}
(s : Finset α)
(f : α → β)
[CommMonoid β]
:
theorem
Finset.sum_coe_sort
{α : Type u_3}
{β : Type u_4}
(s : Finset α)
(f : α → β)
[AddCommMonoid β]
:
theorem
Finset.prod_finset_coe
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(f : α → β)
(s : Finset α)
:
∏ i : ↑↑s, f ↑i = ∏ i ∈ s, f i
theorem
Finset.sum_finset_coe
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(f : α → β)
(s : Finset α)
:
∑ i : ↑↑s, f ↑i = ∑ i ∈ s, f i
theorem
Finset.prod_preimage'
{ι : Type u_1}
{κ : Type u_2}
{β : Type u_4}
[CommMonoid β]
(f : ι → κ)
[DecidablePred fun (x : κ) => x ∈ Set.range f]
(s : Finset κ)
(hf : Set.InjOn f (f ⁻¹' ↑s))
(g : κ → β)
:
∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ Finset.filter (fun (x : κ) => x ∈ Set.range f) s, g x
theorem
Finset.sum_preimage'
{ι : Type u_1}
{κ : Type u_2}
{β : Type u_4}
[AddCommMonoid β]
(f : ι → κ)
[DecidablePred fun (x : κ) => x ∈ Set.range f]
(s : Finset κ)
(hf : Set.InjOn f (f ⁻¹' ↑s))
(g : κ → β)
:
∑ x ∈ s.preimage f hf, g (f x) = ∑ x ∈ Finset.filter (fun (x : κ) => x ∈ Set.range f) s, g x
theorem
Finset.prod_preimage_of_bij
{ι : Type u_1}
{κ : Type u_2}
{β : Type u_4}
[CommMonoid β]
(f : ι → κ)
(s : Finset κ)
(hf : Set.BijOn f (f ⁻¹' ↑s) ↑s)
(g : κ → β)
:
∏ x ∈ s.preimage f ⋯, g (f x) = ∏ x ∈ s, g x
theorem
Finset.sum_preimage_of_bij
{ι : Type u_1}
{κ : Type u_2}
{β : Type u_4}
[AddCommMonoid β]
(f : ι → κ)
(s : Finset κ)
(hf : Set.BijOn f (f ⁻¹' ↑s) ↑s)
(g : κ → β)
:
∑ x ∈ s.preimage f ⋯, g (f x) = ∑ x ∈ s, g x
theorem
Finset.prod_set_coe
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[CommMonoid β]
(s : Set α)
[Fintype ↑s]
:
∏ i : ↑s, f ↑i = ∏ i ∈ s.toFinset, f i
theorem
Finset.sum_set_coe
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[AddCommMonoid β]
(s : Set α)
[Fintype ↑s]
:
∑ i : ↑s, f ↑i = ∑ i ∈ s.toFinset, f i
theorem
Finset.prod_congr_set
{α : Type u_6}
[CommMonoid α]
{β : Type u_7}
[Fintype β]
(s : Set β)
[DecidablePred fun (x : β) => x ∈ s]
(f : β → α)
(g : ↑s → α)
(w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩)
(w' : ∀ x ∉ s, f x = 1)
:
Finset.univ.prod f = Finset.univ.prod g
The product of a function g defined only on a set s is equal to
the product of a function f defined everywhere,
as long as f and g agree on s, and f = 1 off s.
theorem
Finset.sum_congr_set
{α : Type u_6}
[AddCommMonoid α]
{β : Type u_7}
[Fintype β]
(s : Set β)
[DecidablePred fun (x : β) => x ∈ s]
(f : β → α)
(g : ↑s → α)
(w : ∀ (x : β) (h : x ∈ s), f x = g ⟨x, h⟩)
(w' : ∀ x ∉ s, f x = 0)
:
Finset.univ.sum f = Finset.univ.sum g
The sum of a function g defined only on a set s is equal to
the sum of a function f defined everywhere,
as long as f and g agree on s, and f = 0 off s.
theorem
Finset.prod_apply_dite
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[CommMonoid β]
{s : Finset α}
{p : α → Prop}
{hp : DecidablePred p}
[DecidablePred fun (x : α) => ¬p x]
(f : (x : α) → p x → γ)
(g : (x : α) → ¬p x → γ)
(h : γ → β)
:
∏ x ∈ s, h (if hx : p x then f x hx else g x hx) = (∏ x : { x : α // x ∈ Finset.filter (fun (x : α) => p x) s }, h (f ↑x ⋯)) * ∏ x : { x : α // x ∈ Finset.filter (fun (x : α) => ¬p x) s }, h (g ↑x ⋯)
theorem
Finset.sum_apply_dite
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddCommMonoid β]
{s : Finset α}
{p : α → Prop}
{hp : DecidablePred p}
[DecidablePred fun (x : α) => ¬p x]
(f : (x : α) → p x → γ)
(g : (x : α) → ¬p x → γ)
(h : γ → β)
:
∑ x ∈ s, h (if hx : p x then f x hx else g x hx) = ∑ x : { x : α // x ∈ Finset.filter (fun (x : α) => p x) s }, h (f ↑x ⋯) + ∑ x : { x : α // x ∈ Finset.filter (fun (x : α) => ¬p x) s }, h (g ↑x ⋯)
theorem
Finset.prod_apply_ite
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[CommMonoid β]
{s : Finset α}
{p : α → Prop}
{_hp : DecidablePred p}
(f g : α → γ)
(h : γ → β)
:
∏ x ∈ s, h (if p x then f x else g x) = (∏ x ∈ Finset.filter (fun (x : α) => p x) s, h (f x)) * ∏ x ∈ Finset.filter (fun (x : α) => ¬p x) s, h (g x)
theorem
Finset.sum_apply_ite
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddCommMonoid β]
{s : Finset α}
{p : α → Prop}
{_hp : DecidablePred p}
(f g : α → γ)
(h : γ → β)
:
∑ x ∈ s, h (if p x then f x else g x) = ∑ x ∈ Finset.filter (fun (x : α) => p x) s, h (f x) + ∑ x ∈ Finset.filter (fun (x : α) => ¬p x) s, h (g x)
theorem
Finset.prod_dite
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
{s : Finset α}
{p : α → Prop}
{hp : DecidablePred p}
(f : (x : α) → p x → β)
(g : (x : α) → ¬p x → β)
:
(∏ x ∈ s, if hx : p x then f x hx else g x hx) = (∏ x : { x : α // x ∈ Finset.filter (fun (x : α) => p x) s }, f ↑x ⋯) * ∏ x : { x : α // x ∈ Finset.filter (fun (x : α) => ¬p x) s }, g ↑x ⋯
theorem
Finset.sum_dite
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
{s : Finset α}
{p : α → Prop}
{hp : DecidablePred p}
(f : (x : α) → p x → β)
(g : (x : α) → ¬p x → β)
:
(∑ x ∈ s, if hx : p x then f x hx else g x hx) = ∑ x : { x : α // x ∈ Finset.filter (fun (x : α) => p x) s }, f ↑x ⋯ + ∑ x : { x : α // x ∈ Finset.filter (fun (x : α) => ¬p x) s }, g ↑x ⋯
theorem
Finset.prod_ite
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
{s : Finset α}
{p : α → Prop}
{hp : DecidablePred p}
(f g : α → β)
:
(∏ x ∈ s, if p x then f x else g x) = (∏ x ∈ Finset.filter (fun (x : α) => p x) s, f x) * ∏ x ∈ Finset.filter (fun (x : α) => ¬p x) s, g x
theorem
Finset.sum_ite
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
{s : Finset α}
{p : α → Prop}
{hp : DecidablePred p}
(f g : α → β)
:
(∑ x ∈ s, if p x then f x else g x) = ∑ x ∈ Finset.filter (fun (x : α) => p x) s, f x + ∑ x ∈ Finset.filter (fun (x : α) => ¬p x) s, g x
theorem
Finset.prod_dite_of_false
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[CommMonoid β]
{p : α → Prop}
{x✝ : DecidablePred p}
(h : ∀ i ∈ s, ¬p i)
(f : (i : α) → p i → β)
(g : (i : α) → ¬p i → β)
:
theorem
Finset.sum_dite_of_false
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[AddCommMonoid β]
{p : α → Prop}
{x✝ : DecidablePred p}
(h : ∀ i ∈ s, ¬p i)
(f : (i : α) → p i → β)
(g : (i : α) → ¬p i → β)
:
theorem
Finset.prod_ite_of_false
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[CommMonoid β]
{p : α → Prop}
{x✝ : DecidablePred p}
(h : ∀ x ∈ s, ¬p x)
(f g : α → β)
:
(∏ x ∈ s, if p x then f x else g x) = ∏ x ∈ s, g x
theorem
Finset.sum_ite_of_false
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[AddCommMonoid β]
{p : α → Prop}
{x✝ : DecidablePred p}
(h : ∀ x ∈ s, ¬p x)
(f g : α → β)
:
(∑ x ∈ s, if p x then f x else g x) = ∑ x ∈ s, g x
theorem
Finset.prod_dite_of_true
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[CommMonoid β]
{p : α → Prop}
{x✝ : DecidablePred p}
(h : ∀ i ∈ s, p i)
(f : (i : α) → p i → β)
(g : (i : α) → ¬p i → β)
:
theorem
Finset.sum_dite_of_true
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[AddCommMonoid β]
{p : α → Prop}
{x✝ : DecidablePred p}
(h : ∀ i ∈ s, p i)
(f : (i : α) → p i → β)
(g : (i : α) → ¬p i → β)
:
theorem
Finset.prod_ite_of_true
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[CommMonoid β]
{p : α → Prop}
{x✝ : DecidablePred p}
(h : ∀ x ∈ s, p x)
(f g : α → β)
:
(∏ x ∈ s, if p x then f x else g x) = ∏ x ∈ s, f x
theorem
Finset.sum_ite_of_true
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[AddCommMonoid β]
{p : α → Prop}
{x✝ : DecidablePred p}
(h : ∀ x ∈ s, p x)
(f g : α → β)
:
(∑ x ∈ s, if p x then f x else g x) = ∑ x ∈ s, f x
theorem
Finset.prod_apply_ite_of_false
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{s : Finset α}
[CommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(f g : α → γ)
(k : γ → β)
(h : ∀ x ∈ s, ¬p x)
:
∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (g x)
theorem
Finset.sum_apply_ite_of_false
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{s : Finset α}
[AddCommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(f g : α → γ)
(k : γ → β)
(h : ∀ x ∈ s, ¬p x)
:
∑ x ∈ s, k (if p x then f x else g x) = ∑ x ∈ s, k (g x)
theorem
Finset.prod_apply_ite_of_true
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{s : Finset α}
[CommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(f g : α → γ)
(k : γ → β)
(h : ∀ x ∈ s, p x)
:
∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (f x)
theorem
Finset.sum_apply_ite_of_true
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{s : Finset α}
[AddCommMonoid β]
{p : α → Prop}
{hp : DecidablePred p}
(f g : α → γ)
(k : γ → β)
(h : ∀ x ∈ s, p x)
:
∑ x ∈ s, k (if p x then f x else g x) = ∑ x ∈ s, k (f x)
theorem
Finset.prod_extend_by_one
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
:
theorem
Finset.sum_extend_by_zero
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
:
@[simp]
theorem
Finset.prod_ite_mem
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(s t : Finset α)
(f : α → β)
:
@[simp]
theorem
Finset.sum_ite_mem
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s t : Finset α)
(f : α → β)
:
@[simp]
theorem
Finset.prod_dite_eq
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : (x : α) → a = x → β)
:
@[simp]
theorem
Finset.sum_dite_eq
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : (x : α) → a = x → β)
:
@[simp]
theorem
Finset.prod_dite_eq'
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : (x : α) → x = a → β)
:
@[simp]
theorem
Finset.sum_dite_eq'
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : (x : α) → x = a → β)
:
@[simp]
theorem
Finset.prod_ite_eq
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : α → β)
:
@[simp]
theorem
Finset.sum_ite_eq
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : α → β)
:
@[simp]
theorem
Finset.prod_ite_eq'
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(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.
@[simp]
theorem
Finset.sum_ite_eq'
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(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.
theorem
Finset.prod_ite_eq_of_mem
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : α → β)
(h : a ∈ s)
:
theorem
Finset.sum_ite_eq_of_mem
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : α → β)
(h : a ∈ s)
:
theorem
Finset.prod_ite_eq_of_mem'
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : α → β)
(h : a ∈ s)
:
The difference with Finset.prod_ite_eq_of_mem is that the arguments to Eq are swapped.
theorem
Finset.sum_ite_eq_of_mem'
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(a : α)
(b : α → β)
(h : a ∈ s)
:
theorem
Finset.prod_ite_index
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(p : Prop)
[Decidable p]
(s t : Finset α)
(f : α → β)
:
∏ x ∈ if p then s else t, f x = if p then ∏ x ∈ s, f x else ∏ x ∈ t, f x
theorem
Finset.sum_ite_index
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(p : Prop)
[Decidable p]
(s t : Finset α)
(f : α → β)
:
∑ x ∈ if p then s else t, f x = if p then ∑ x ∈ s, f x else ∑ x ∈ t, f x
@[simp]
theorem
Finset.prod_ite_irrel
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(p : Prop)
[Decidable p]
(s : Finset α)
(f g : α → β)
:
(∏ x ∈ s, if p then f x else g x) = if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x
@[simp]
theorem
Finset.sum_ite_irrel
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(p : Prop)
[Decidable p]
(s : Finset α)
(f g : α → β)
:
(∑ x ∈ s, if p then f x else g x) = if p then ∑ x ∈ s, f x else ∑ x ∈ s, g x
@[simp]
theorem
Finset.prod_dite_irrel
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(p : Prop)
[Decidable p]
(s : Finset α)
(f : p → α → β)
(g : ¬p → α → β)
:
(∏ x ∈ s, if h : p then f h x else g h x) = if h : p then ∏ x ∈ s, f h x else ∏ x ∈ s, g h x
@[simp]
theorem
Finset.sum_dite_irrel
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(p : Prop)
[Decidable p]
(s : Finset α)
(f : p → α → β)
(g : ¬p → α → β)
:
(∑ x ∈ s, if h : p then f h x else g h x) = if h : p then ∑ x ∈ s, f h x else ∑ x ∈ s, g h x
@[simp]
theorem
Finset.prod_pi_mulSingle'
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(a : α)
(x : β)
(s : Finset α)
:
∏ a' ∈ s, Pi.mulSingle a x a' = if a ∈ s then x else 1
@[simp]
theorem
Finset.sum_pi_single'
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(a : α)
(x : β)
(s : Finset α)
:
@[simp]
theorem
Finset.prod_pi_mulSingle
{α : Type u_3}
{β : α → Type u_6}
[DecidableEq α]
[(a : α) → CommMonoid (β a)]
(a : α)
(f : (a : α) → β a)
(s : Finset α)
:
∏ a' ∈ s, Pi.mulSingle a' (f a') a = if a ∈ s then f a else 1
@[simp]
theorem
Finset.sum_pi_single
{α : Type u_3}
{β : α → Type u_6}
[DecidableEq α]
[(a : α) → AddCommMonoid (β a)]
(a : α)
(f : (a : α) → β a)
(s : Finset α)
:
theorem
Finset.mulSupport_prod
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(s : Finset ι)
(f : ι → α → β)
:
(Function.mulSupport fun (x : α) => ∏ i ∈ s, f i x) ⊆ ⋃ i ∈ s, Function.mulSupport (f i)
theorem
Finset.support_sum
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset ι)
(f : ι → α → β)
:
(Function.support fun (x : α) => ∑ i ∈ s, f i x) ⊆ ⋃ i ∈ s, Function.support (f i)
theorem
Finset.prod_mulIndicator_subset_of_eq_one
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[One α]
(f : ι → α)
(g : ι → α → β)
{s t : Finset ι}
(h : s ⊆ t)
(hg : ∀ (a : ι), g a 1 = 1)
:
∏ i ∈ t, g i ((↑s).mulIndicator f i) = ∏ i ∈ s, g i (f i)
Consider a product of g i (f i) over a finset. Suppose g is a function such as
n ↦ (· ^ n), which maps a second argument of 1 to 1. Then if f is replaced by the
corresponding multiplicative indicator function, the finset may be replaced by a possibly larger
finset without changing the value of the product.
theorem
Finset.sum_indicator_subset_of_eq_zero
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[Zero α]
(f : ι → α)
(g : ι → α → β)
{s t : Finset ι}
(h : s ⊆ t)
(hg : ∀ (a : ι), g a 0 = 0)
:
∑ i ∈ t, g i ((↑s).indicator f i) = ∑ i ∈ s, g i (f i)
Consider a sum of g i (f i) over a finset. Suppose g is a function such as
n ↦ (n • ·), which maps a second argument of 0 to 0 (or a weighted sum of f i * h i or
f i • h i, where f gives the weights that are multiplied by some other function h). Then if
f is replaced by the corresponding indicator function, the finset may be replaced by a possibly
larger finset without changing the value of the sum.
theorem
Finset.prod_mulIndicator_subset
{ι : Type u_1}
{β : Type u_4}
[CommMonoid β]
(f : ι → β)
{s t : Finset ι}
(h : s ⊆ t)
:
∏ i ∈ t, (↑s).mulIndicator f i = ∏ i ∈ s, f i
Taking the product of an indicator function over a possibly larger finset is the same as taking the original function over the original finset.
theorem
Finset.sum_indicator_subset
{ι : Type u_1}
{β : Type u_4}
[AddCommMonoid β]
(f : ι → β)
{s t : Finset ι}
(h : s ⊆ t)
:
∑ i ∈ t, (↑s).indicator f i = ∑ i ∈ s, f i
Summing an indicator function over a possibly larger Finset is the same as summing
the original function over the original finset.
theorem
Finset.prod_mulIndicator_eq_prod_filter
{ι : Type u_1}
{β : Type u_4}
[CommMonoid β]
{κ : Type u_6}
(s : Finset ι)
(f : ι → κ → β)
(t : ι → Set κ)
(g : ι → κ)
[DecidablePred fun (i : ι) => g i ∈ t i]
:
∏ i ∈ s, (t i).mulIndicator (f i) (g i) = ∏ i ∈ Finset.filter (fun (i : ι) => g i ∈ t i) s, f i (g i)
theorem
Finset.sum_indicator_eq_sum_filter
{ι : Type u_1}
{β : Type u_4}
[AddCommMonoid β]
{κ : Type u_6}
(s : Finset ι)
(f : ι → κ → β)
(t : ι → Set κ)
(g : ι → κ)
[DecidablePred fun (i : ι) => g i ∈ t i]
:
∑ i ∈ s, (t i).indicator (f i) (g i) = ∑ i ∈ Finset.filter (fun (i : ι) => g i ∈ t i) s, f i (g i)
theorem
Finset.prod_mulIndicator_eq_prod_inter
{ι : Type u_1}
{β : Type u_4}
[CommMonoid β]
[DecidableEq ι]
(s t : Finset ι)
(f : ι → β)
:
theorem
Finset.sum_indicator_eq_sum_inter
{ι : Type u_1}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq ι]
(s t : Finset ι)
(f : ι → β)
:
theorem
Finset.mulIndicator_prod
{ι : Type u_1}
{β : Type u_4}
[CommMonoid β]
{κ : Type u_6}
(s : Finset ι)
(t : Set κ)
(f : ι → κ → β)
:
t.mulIndicator (∏ i ∈ s, f i) = ∏ i ∈ s, t.mulIndicator (f i)
theorem
Finset.indicator_sum
{ι : Type u_1}
{β : Type u_4}
[AddCommMonoid β]
{κ : Type u_6}
(s : Finset ι)
(t : Set κ)
(f : ι → κ → β)
:
t.indicator (∑ i ∈ s, f i) = ∑ i ∈ s, t.indicator (f i)
theorem
Finset.mulIndicator_biUnion
{ι : Type u_1}
{β : Type u_4}
[CommMonoid β]
{κ : Type u_7}
(s : Finset ι)
(t : ι → Set κ)
{f : κ → β}
(hs : (↑s).PairwiseDisjoint t)
:
(⋃ i ∈ s, t i).mulIndicator f = fun (a : κ) => ∏ i ∈ s, (t i).mulIndicator f a
theorem
Finset.indicator_biUnion
{ι : Type u_1}
{β : Type u_4}
[AddCommMonoid β]
{κ : Type u_7}
(s : Finset ι)
(t : ι → Set κ)
{f : κ → β}
(hs : (↑s).PairwiseDisjoint t)
:
(⋃ i ∈ s, t i).indicator f = fun (a : κ) => ∑ i ∈ s, (t i).indicator f a
theorem
Finset.mulIndicator_biUnion_apply
{ι : Type u_1}
{β : Type u_4}
[CommMonoid β]
{κ : Type u_7}
(s : Finset ι)
(t : ι → Set κ)
{f : κ → β}
(h : (↑s).PairwiseDisjoint t)
(x : κ)
:
(⋃ i ∈ s, t i).mulIndicator f x = ∏ i ∈ s, (t i).mulIndicator f x
theorem
Finset.indicator_biUnion_apply
{ι : Type u_1}
{β : Type u_4}
[AddCommMonoid β]
{κ : Type u_7}
(s : Finset ι)
(t : ι → Set κ)
{f : κ → β}
(h : (↑s).PairwiseDisjoint t)
(x : κ)
:
(⋃ i ∈ s, t i).indicator f x = ∑ i ∈ s, (t i).indicator f x
theorem
Finset.prod_bij_ne_one
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[CommMonoid β]
{s : Finset α}
{t : Finset γ}
{f : α → β}
{g : γ → β}
(i : (a : α) → a ∈ s → f a ≠ 1 → γ)
(hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t)
(i_inj :
∀ (a₁ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : α) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂)
(i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b)
(h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂))
:
∏ x ∈ s, f x = ∏ x ∈ t, g x
theorem
Finset.sum_bij_ne_zero
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddCommMonoid β]
{s : Finset α}
{t : Finset γ}
{f : α → β}
{g : γ → β}
(i : (a : α) → a ∈ s → f a ≠ 0 → γ)
(hi : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), i a h₁ h₂ ∈ t)
(i_inj :
∀ (a₁ : α) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 0) (a₂ : α) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 0),
i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂)
(i_surj : ∀ b ∈ t, g b ≠ 0 → ∃ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), i a h₁ h₂ = b)
(h : ∀ (a : α) (h₁ : a ∈ s) (h₂ : f a ≠ 0), f a = g (i a h₁ h₂))
:
∑ x ∈ s, f x = ∑ x ∈ t, g x
theorem
Finset.nonempty_of_prod_ne_one
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommMonoid β]
(h : ∏ x ∈ s, f x ≠ 1)
:
s.Nonempty
theorem
Finset.nonempty_of_sum_ne_zero
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
(h : ∑ x ∈ s, f x ≠ 0)
:
s.Nonempty
theorem
Finset.exists_ne_one_of_prod_ne_one
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommMonoid β]
(h : ∏ x ∈ s, f x ≠ 1)
:
∃ a ∈ s, f a ≠ 1
theorem
Finset.exists_ne_zero_of_sum_ne_zero
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
(h : ∑ x ∈ s, f x ≠ 0)
:
∃ a ∈ s, f a ≠ 0
theorem
Finset.prod_range_succ_comm
{β : Type u_4}
[CommMonoid β]
(f : ℕ → β)
(n : ℕ)
:
∏ x ∈ Finset.range (n + 1), f x = f n * ∏ x ∈ Finset.range n, f x
theorem
Finset.sum_range_succ_comm
{β : Type u_4}
[AddCommMonoid β]
(f : ℕ → β)
(n : ℕ)
:
∑ x ∈ Finset.range (n + 1), f x = f n + ∑ x ∈ Finset.range n, f x
theorem
Finset.prod_range_succ
{β : Type u_4}
[CommMonoid β]
(f : ℕ → β)
(n : ℕ)
:
∏ x ∈ Finset.range (n + 1), f x = (∏ x ∈ Finset.range n, f x) * f n
theorem
Finset.sum_range_succ
{β : Type u_4}
[AddCommMonoid β]
(f : ℕ → β)
(n : ℕ)
:
∑ x ∈ Finset.range (n + 1), f x = ∑ x ∈ Finset.range n, f x + f n
theorem
Finset.prod_range_succ'
{β : Type u_4}
[CommMonoid β]
(f : ℕ → β)
(n : ℕ)
:
∏ k ∈ Finset.range (n + 1), f k = (∏ k ∈ Finset.range n, f (k + 1)) * f 0
theorem
Finset.sum_range_succ'
{β : Type u_4}
[AddCommMonoid β]
(f : ℕ → β)
(n : ℕ)
:
∑ k ∈ Finset.range (n + 1), f k = ∑ k ∈ Finset.range n, f (k + 1) + f 0
theorem
Finset.eventually_constant_prod
{β : Type u_4}
[CommMonoid β]
{u : ℕ → β}
{N : ℕ}
(hu : ∀ n ≥ N, u n = 1)
{n : ℕ}
(hn : N ≤ n)
:
∏ k ∈ Finset.range n, u k = ∏ k ∈ Finset.range N, u k
theorem
Finset.eventually_constant_sum
{β : Type u_4}
[AddCommMonoid β]
{u : ℕ → β}
{N : ℕ}
(hu : ∀ n ≥ N, u n = 0)
{n : ℕ}
(hn : N ≤ n)
:
∑ k ∈ Finset.range n, u k = ∑ k ∈ Finset.range N, u k
theorem
Finset.prod_range_add
{β : Type u_4}
[CommMonoid β]
(f : ℕ → β)
(n m : ℕ)
:
∏ x ∈ Finset.range (n + m), f x = (∏ x ∈ Finset.range n, f x) * ∏ x ∈ Finset.range m, f (n + x)
theorem
Finset.sum_range_add
{β : Type u_4}
[AddCommMonoid β]
(f : ℕ → β)
(n m : ℕ)
:
∑ x ∈ Finset.range (n + m), f x = ∑ x ∈ Finset.range n, f x + ∑ x ∈ Finset.range m, f (n + x)
theorem
Finset.prod_range_add_div_prod_range
{α : Type u_6}
[CommGroup α]
(f : ℕ → α)
(n m : ℕ)
:
(∏ k ∈ Finset.range (n + m), f k) / ∏ k ∈ Finset.range n, f k = ∏ k ∈ Finset.range m, f (n + k)
theorem
Finset.sum_range_add_sub_sum_range
{α : Type u_6}
[AddCommGroup α]
(f : ℕ → α)
(n m : ℕ)
:
∑ k ∈ Finset.range (n + m), f k - ∑ k ∈ Finset.range n, f k = ∑ k ∈ Finset.range m, f (n + k)
theorem
Finset.prod_range_zero
{β : Type u_4}
[CommMonoid β]
(f : ℕ → β)
:
∏ k ∈ Finset.range 0, f k = 1
theorem
Finset.sum_range_zero
{β : Type u_4}
[AddCommMonoid β]
(f : ℕ → β)
:
∑ k ∈ Finset.range 0, f k = 0
theorem
Finset.prod_range_one
{β : Type u_4}
[CommMonoid β]
(f : ℕ → β)
:
∏ k ∈ Finset.range 1, f k = f 0
theorem
Finset.sum_range_one
{β : Type u_4}
[AddCommMonoid β]
(f : ℕ → β)
:
∑ k ∈ Finset.range 1, f k = f 0
theorem
Finset.prod_list_map_count
{α : Type u_3}
[DecidableEq α]
(l : List α)
{M : Type u_6}
[CommMonoid M]
(f : α → M)
:
(List.map f l).prod = ∏ m ∈ l.toFinset, f m ^ List.count m l
theorem
Finset.sum_list_map_count
{α : Type u_3}
[DecidableEq α]
(l : List α)
{M : Type u_6}
[AddCommMonoid M]
(f : α → M)
:
(List.map f l).sum = ∑ m ∈ l.toFinset, List.count m l • f m
theorem
Finset.prod_list_count
{α : Type u_3}
[DecidableEq α]
[CommMonoid α]
(s : List α)
:
s.prod = ∏ m ∈ s.toFinset, m ^ List.count m s
theorem
Finset.sum_list_count
{α : Type u_3}
[DecidableEq α]
[AddCommMonoid α]
(s : List α)
:
s.sum = ∑ m ∈ s.toFinset, List.count m s • m
theorem
Finset.prod_list_count_of_subset
{α : Type u_3}
[DecidableEq α]
[CommMonoid α]
(m : List α)
(s : Finset α)
(hs : m.toFinset ⊆ s)
:
m.prod = ∏ i ∈ s, i ^ List.count i m
theorem
Finset.sum_list_count_of_subset
{α : Type u_3}
[DecidableEq α]
[AddCommMonoid α]
(m : List α)
(s : Finset α)
(hs : m.toFinset ⊆ s)
:
m.sum = ∑ i ∈ s, List.count i m • i
theorem
Finset.sum_filter_count_eq_countP
{α : Type u_3}
[DecidableEq α]
(p : α → Prop)
[DecidablePred p]
(l : List α)
:
∑ x ∈ Finset.filter (fun (x : α) => p x) l.toFinset, List.count x l = List.countP (fun (b : α) => decide (p b)) l
theorem
Finset.prod_multiset_map_count
{α : Type u_3}
[DecidableEq α]
(s : Multiset α)
{M : Type u_6}
[CommMonoid M]
(f : α → M)
:
(Multiset.map f s).prod = ∏ m ∈ s.toFinset, f m ^ Multiset.count m s
theorem
Finset.sum_multiset_map_count
{α : Type u_3}
[DecidableEq α]
(s : Multiset α)
{M : Type u_6}
[AddCommMonoid M]
(f : α → M)
:
(Multiset.map f s).sum = ∑ m ∈ s.toFinset, Multiset.count m s • f m
theorem
Finset.prod_multiset_count
{α : Type u_3}
[DecidableEq α]
[CommMonoid α]
(s : Multiset α)
:
s.prod = ∏ m ∈ s.toFinset, m ^ Multiset.count m s
theorem
Finset.sum_multiset_count
{α : Type u_3}
[DecidableEq α]
[AddCommMonoid α]
(s : Multiset α)
:
s.sum = ∑ m ∈ s.toFinset, Multiset.count m s • m
theorem
Finset.prod_multiset_count_of_subset
{α : Type u_3}
[DecidableEq α]
[CommMonoid α]
(m : Multiset α)
(s : Finset α)
(hs : m.toFinset ⊆ s)
:
m.prod = ∏ i ∈ s, i ^ Multiset.count i m
theorem
Finset.sum_multiset_count_of_subset
{α : Type u_3}
[DecidableEq α]
[AddCommMonoid α]
(m : Multiset α)
(s : Finset α)
(hs : m.toFinset ⊆ s)
:
m.sum = ∑ i ∈ s, Multiset.count i m • i
theorem
Finset.prod_mem_multiset
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(m : Multiset α)
(f : { x : α // x ∈ m } → β)
(g : α → β)
(hfg : ∀ (x : { x : α // x ∈ m }), f x = g ↑x)
:
theorem
Finset.sum_mem_multiset
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(m : Multiset α)
(f : { x : α // x ∈ m } → β)
(g : α → β)
(hfg : ∀ (x : { x : α // x ∈ m }), f x = g ↑x)
:
theorem
Finset.prod_induction
{α : Type u_3}
{s : Finset α}
{M : Type u_6}
[CommMonoid M]
(f : α → M)
(p : M → Prop)
(hom : ∀ (a b : M), p a → p b → p (a * b))
(unit : p 1)
(base : ∀ x ∈ s, p (f x))
:
p (∏ x ∈ 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 u_3}
{s : Finset α}
{M : Type u_6}
[AddCommMonoid M]
(f : α → M)
(p : M → Prop)
(hom : ∀ (a b : M), p a → p b → p (a + b))
(unit : p 0)
(base : ∀ x ∈ s, p (f x))
:
p (∑ x ∈ 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 u_3}
{s : Finset α}
{M : Type u_6}
[CommMonoid M]
(f : α → M)
(p : M → Prop)
(hom : ∀ (a b : M), p a → p b → p (a * b))
(nonempty : s.Nonempty)
(base : ∀ x ∈ s, p (f x))
:
p (∏ x ∈ 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_nonempty
{α : Type u_3}
{s : Finset α}
{M : Type u_6}
[AddCommMonoid M]
(f : α → M)
(p : M → Prop)
(hom : ∀ (a b : M), p a → p b → p (a + b))
(nonempty : s.Nonempty)
(base : ∀ x ∈ s, p (f x))
:
p (∑ x ∈ 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_range_induction
{β : Type u_4}
[CommMonoid β]
(f s : ℕ → β)
(base : s 0 = 1)
(step : ∀ (n : ℕ), s (n + 1) = s n * f n)
(n : ℕ)
:
∏ k ∈ Finset.range n, f k = s n
For any product along {0, ..., n - 1} of a commutative-monoid-valued function, we can verify
that it's equal to a different function just by checking ratios of adjacent terms.
This is a multiplicative discrete analogue of the fundamental theorem of calculus.
theorem
Finset.sum_range_induction
{β : Type u_4}
[AddCommMonoid β]
(f s : ℕ → β)
(base : s 0 = 0)
(step : ∀ (n : ℕ), s (n + 1) = s n + f n)
(n : ℕ)
:
∑ k ∈ Finset.range n, f k = s n
For any sum along {0, ..., n - 1} of a commutative-monoid-valued function, we can
verify that it's equal to a different function just by checking differences of adjacent terms.
This is a discrete analogue of the fundamental theorem of calculus.
theorem
Finset.sum_range_sub
{M : Type u_6}
[AddCommGroup M]
(f : ℕ → M)
(n : ℕ)
:
∑ i ∈ Finset.range n, (f (i + 1) - f i) = f n - f 0
A telescoping sum along {0, ..., n - 1} of an additive commutative group valued
function reduces to the difference of the last and first terms.
theorem
Finset.sum_range_sub'
{M : Type u_6}
[AddCommGroup M]
(f : ℕ → M)
(n : ℕ)
:
∑ i ∈ Finset.range n, (f i - f (i + 1)) = f 0 - f n
theorem
Finset.eq_sum_range_sub
{M : Type u_6}
[AddCommGroup M]
(f : ℕ → M)
(n : ℕ)
:
f n = f 0 + ∑ i ∈ Finset.range n, (f (i + 1) - f i)
theorem
Finset.sum_range_tsub
{α : Type u_3}
[AddCommMonoid α]
[PartialOrder α]
[Sub α]
[OrderedSub α]
[AddLeftMono α]
[AddLeftReflectLE α]
[ExistsAddOfLE α]
{f : ℕ → α}
(h : Monotone f)
(n : ℕ)
:
∑ i ∈ Finset.range n, (f (i + 1) - f i) = f n - f 0
A telescoping sum along {0, ..., n-1} of an ℕ-valued function
reduces to the difference of the last and first terms
when the function we are summing is monotone.
theorem
Finset.sum_tsub_distrib
{ι : Type u_1}
{α : Type u_3}
[AddCommMonoid α]
[PartialOrder α]
[ExistsAddOfLE α]
[CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2]
[Sub α]
[OrderedSub α]
(s : Finset ι)
{f g : ι → α}
(hfg : ∀ x ∈ s, g x ≤ f x)
:
@[simp]
@[simp]
theorem
Finset.prod_eq_pow_card
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommMonoid β]
{b : β}
(hf : ∀ a ∈ s, f a = b)
:
theorem
Finset.sum_eq_card_nsmul
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
{b : β}
(hf : ∀ a ∈ s, f a = b)
:
theorem
Finset.pow_card_mul_prod
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommMonoid β]
{b : β}
:
theorem
Finset.card_nsmul_add_sum
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
{b : β}
:
theorem
Finset.prod_mul_pow_card
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommMonoid β]
{b : β}
:
theorem
Finset.sum_add_card_nsmul
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
{b : β}
:
theorem
Finset.pow_eq_prod_const
{β : Type u_4}
[CommMonoid β]
(b : β)
(n : ℕ)
:
b ^ n = ∏ _k ∈ Finset.range n, b
theorem
Finset.nsmul_eq_sum_const
{β : Type u_4}
[AddCommMonoid β]
(b : β)
(n : ℕ)
:
n • b = ∑ _k ∈ Finset.range n, b
theorem
Finset.prod_pow
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(s : Finset α)
(n : ℕ)
(f : α → β)
:
theorem
Finset.sum_nsmul
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset α)
(n : ℕ)
(f : α → β)
:
theorem
Finset.prod_pow_eq_pow_sum
{ι : Type u_1}
{β : Type u_4}
[CommMonoid β]
(s : Finset ι)
(f : ι → ℕ)
(a : β)
:
theorem
Finset.sum_nsmul_assoc
{ι : Type u_1}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset ι)
(f : ι → ℕ)
(a : β)
:
theorem
Finset.prod_powersetCard
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(n : ℕ)
(s : Finset α)
(f : ℕ → β)
:
∏ t ∈ Finset.powersetCard n s, f t.card = f n ^ s.card.choose n
A product over Finset.powersetCard which only depends on the size of the sets is constant.
theorem
Finset.sum_powersetCard
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(n : ℕ)
(s : Finset α)
(f : ℕ → β)
:
∑ t ∈ Finset.powersetCard n s, f t.card = s.card.choose n • f n
A sum over Finset.powersetCard which only depends on the size of the sets is constant.
theorem
Finset.prod_flip
{β : Type u_4}
[CommMonoid β]
{n : ℕ}
(f : ℕ → β)
:
∏ r ∈ Finset.range (n + 1), f (n - r) = ∏ k ∈ Finset.range (n + 1), f k
theorem
Finset.sum_flip
{β : Type u_4}
[AddCommMonoid β]
{n : ℕ}
(f : ℕ → β)
:
∑ r ∈ Finset.range (n + 1), f (n - r) = ∑ k ∈ Finset.range (n + 1), f k
theorem
Finset.prod_involution
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommMonoid β]
(g : (a : α) → a ∈ s → α)
(hg₁ : ∀ (a : α) (ha : a ∈ s), f a * f (g a ha) = 1)
(hg₃ : ∀ (a : α) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a)
(g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s)
(hg₄ : ∀ (a : α) (ha : a ∈ s), g (g a ha) ⋯ = a)
:
∏ x ∈ s, f x = 1
The difference with Finset.prod_ninvolution is that the involution is allowed to use
membership of the domain of the product, rather than being a non-dependent function.
theorem
Finset.sum_involution
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
(g : (a : α) → a ∈ s → α)
(hg₁ : ∀ (a : α) (ha : a ∈ s), f a + f (g a ha) = 0)
(hg₃ : ∀ (a : α) (ha : a ∈ s), f a ≠ 0 → g a ha ≠ a)
(g_mem : ∀ (a : α) (ha : a ∈ s), g a ha ∈ s)
(hg₄ : ∀ (a : α) (ha : a ∈ s), g (g a ha) ⋯ = a)
:
∑ x ∈ s, f x = 0
The difference with Finset.sum_ninvolution is that the involution is allowed to use
membership of the domain of the sum, rather than being a non-dependent function.
theorem
Finset.prod_ninvolution
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommMonoid β]
(g : α → α)
(hg₁ : ∀ (a : α), f a * f (g a) = 1)
(hg₂ : ∀ (a : α), f a ≠ 1 → g a ≠ a)
(g_mem : ∀ (a : α), g a ∈ s)
(hg₃ : ∀ (a : α), g (g a) = a)
:
∏ x ∈ s, f x = 1
The difference with Finset.prod_involution is that the involution is a non-dependent function,
rather than being allowed to use membership of the domain of the product.
theorem
Finset.sum_ninvolution
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
(g : α → α)
(hg₁ : ∀ (a : α), f a + f (g a) = 0)
(hg₂ : ∀ (a : α), f a ≠ 0 → g a ≠ a)
(g_mem : ∀ (a : α), g a ∈ s)
(hg₃ : ∀ (a : α), g (g a) = a)
:
∑ x ∈ s, f x = 0
The difference with Finset.sum_involution is that the involution is a non-dependent
function, rather than being allowed to use membership of the domain of the sum.
theorem
Finset.prod_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{s : Finset α}
[CommMonoid β]
[DecidableEq γ]
(f : γ → β)
(g : α → γ)
:
∏ a ∈ s, f (g a) = ∏ b ∈ Finset.image g s, f b ^ (Finset.filter (fun (a : α) => g a = b) s).card
The product of the composition of functions f and g, is the product over b ∈ s.image g of
f b to the power of the cardinality of the fibre of b. See also Finset.prod_image.
theorem
Finset.sum_comp
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{s : Finset α}
[AddCommMonoid β]
[DecidableEq γ]
(f : γ → β)
(g : α → γ)
:
∑ a ∈ s, f (g a) = ∑ b ∈ Finset.image g s, (Finset.filter (fun (a : α) => g a = b) s).card • f b
The sum of the composition of functions f and g, is the sum over b ∈ s.image g
of f b times of the cardinality of the fibre of b. See also Finset.sum_image.
theorem
Finset.prod_piecewise
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(s t : Finset α)
(f g : α → β)
:
theorem
Finset.sum_piecewise
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s t : Finset α)
(f g : α → β)
:
theorem
Finset.prod_inter_mul_prod_diff
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(s t : Finset α)
(f : α → β)
:
theorem
Finset.sum_inter_add_sum_diff
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s t : Finset α)
(f : α → β)
:
theorem
Finset.prod_eq_mul_prod_diff_singleton
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
:
theorem
Finset.sum_eq_add_sum_diff_singleton
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
:
theorem
Finset.prod_eq_prod_diff_singleton_mul
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
:
theorem
Finset.sum_eq_sum_diff_singleton_add
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
:
theorem
Fintype.prod_eq_mul_prod_compl
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
[Fintype α]
(a : α)
(f : α → β)
:
theorem
Fintype.sum_eq_add_sum_compl
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
[Fintype α]
(a : α)
(f : α → β)
:
theorem
Fintype.prod_eq_prod_compl_mul
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
[Fintype α]
(a : α)
(f : α → β)
:
theorem
Fintype.sum_eq_sum_compl_add
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
[Fintype α]
(a : α)
(f : α → β)
:
theorem
Finset.dvd_prod_of_mem
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(f : α → β)
{a : α}
{s : Finset α}
(ha : a ∈ s)
:
f a ∣ ∏ i ∈ s, f i
theorem
Finset.prod_partition
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommMonoid β]
(R : Setoid α)
[DecidableRel ⇑R]
:
∏ x ∈ s, f x = ∏ xbar ∈ Finset.image (Quotient.mk R) s, ∏ y ∈ Finset.filter (fun (y : α) => ⟦y⟧ = xbar) s, f y
A product can be partitioned into a product of products, each equivalent under a setoid.
theorem
Finset.sum_partition
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
(R : Setoid α)
[DecidableRel ⇑R]
:
∑ x ∈ s, f x = ∑ xbar ∈ Finset.image (Quotient.mk R) s, ∑ y ∈ Finset.filter (fun (y : α) => ⟦y⟧ = xbar) s, f y
A sum can be partitioned into a sum of sums, each equivalent under a setoid.
theorem
Finset.prod_cancels_of_partition_cancels
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommMonoid β]
(R : Setoid α)
[DecidableRel ⇑R]
(h : ∀ x ∈ s, ∏ a ∈ Finset.filter (fun (a : α) => R a x) s, f a = 1)
:
∏ x ∈ s, f x = 1
If we can partition a product into subsets that cancel out, then the whole product cancels.
theorem
Finset.sum_cancels_of_partition_cancels
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
(R : Setoid α)
[DecidableRel ⇑R]
(h : ∀ x ∈ s, ∑ a ∈ Finset.filter (fun (a : α) => R a x) s, f a = 0)
:
∑ x ∈ s, f x = 0
If we can partition a sum into subsets that cancel out, then the whole sum cancels.
theorem
Finset.prod_update_of_not_mem
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∉ s)
(f : α → β)
(b : β)
:
∏ x ∈ s, Function.update f i b x = ∏ x ∈ s, f x
theorem
Finset.sum_update_of_not_mem
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∉ s)
(f : α → β)
(b : β)
:
∑ x ∈ s, Function.update f i b x = ∑ x ∈ s, f x
theorem
Finset.prod_update_of_mem
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
(b : β)
:
∏ x ∈ s, Function.update f i b x = b * ∏ x ∈ s \ {i}, f x
theorem
Finset.sum_update_of_mem
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
(b : β)
:
∑ x ∈ s, Function.update f i b x = b + ∑ x ∈ s \ {i}, f x
theorem
Finset.mul_prod_erase
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(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.
See Multiset.prod_map_erase for the Multiset version.
theorem
Finset.add_sum_erase
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
{a : α}
(h : a ∈ s)
:
Taking a sum over s : Finset α is the same as adding the value on a single element
f a to the sum over s.erase a.
See Multiset.sum_map_erase for the Multiset version.
theorem
Finset.prod_erase_mul
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
{a : α}
(h : a ∈ s)
:
A variant of Finset.mul_prod_erase with the multiplication swapped.
theorem
Finset.sum_erase_add
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
{a : α}
(h : a ∈ s)
:
A variant of Finset.add_sum_erase with the addition swapped.
theorem
Finset.prod_erase
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
{f : α → β}
{a : α}
(h : f a = 1)
:
∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x
If a function applied at a point is 1, a product is unchanged by
removing that point, if present, from a Finset.
theorem
Finset.sum_erase
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
{f : α → β}
{a : α}
(h : f a = 0)
:
∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x
If a function applied at a point is 0, a sum is unchanged by
removing that point, if present, from a Finset.
theorem
Finset.prod_ite_one
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(s : Finset α)
(p : α → Prop)
[DecidablePred p]
(h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j)
(a : β)
:
(∏ i ∈ s, if p i then a else 1) = if ∃ i ∈ s, p i then a else 1
See also Finset.prod_ite_zero.
theorem
Finset.sum_ite_zero
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset α)
(p : α → Prop)
[DecidablePred p]
(h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j)
(a : β)
:
(∑ i ∈ s, if p i then a else 0) = if ∃ i ∈ s, p i then a else 0
See also Finset.sum_boole.
theorem
Finset.prod_erase_lt_of_one_lt
{α : Type u_3}
{γ : Type u_6}
[DecidableEq α]
[CommMonoid γ]
[Preorder γ]
[MulLeftStrictMono γ]
{s : Finset α}
{d : α}
(hd : d ∈ s)
{f : α → γ}
(hdf : 1 < f d)
:
∏ m ∈ s.erase d, f m < ∏ m ∈ s, f m
theorem
Finset.sum_erase_lt_of_pos
{α : Type u_3}
{γ : Type u_6}
[DecidableEq α]
[AddCommMonoid γ]
[Preorder γ]
[AddLeftStrictMono γ]
{s : Finset α}
{d : α}
(hd : d ∈ s)
{f : α → γ}
(hdf : 0 < f d)
:
∑ m ∈ s.erase d, f m < ∑ m ∈ s, f m
theorem
Finset.eq_one_of_prod_eq_one
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
{s : Finset α}
{f : α → β}
{a : α}
(hp : ∏ x ∈ s, f x = 1)
(h1 : ∀ x ∈ s, x ≠ a → f x = 1)
(x : α)
:
If a product is 1 and the function is 1 except possibly at one
point, it is 1 everywhere on the Finset.
theorem
Finset.eq_zero_of_sum_eq_zero
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
{s : Finset α}
{f : α → β}
{a : α}
(hp : ∑ x ∈ s, f x = 0)
(h1 : ∀ x ∈ s, x ≠ a → f x = 0)
(x : α)
:
If a sum is 0 and the function is 0 except possibly at one
point, it is 0 everywhere on the Finset.
theorem
Finset.prod_pow_boole
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
(a : α)
:
theorem
Finset.sum_boole_nsmul
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α → β)
(a : α)
:
theorem
Finset.prod_dvd_prod_of_dvd
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
{S : Finset α}
(g1 g2 : α → β)
(h : ∀ a ∈ S, g1 a ∣ g2 a)
:
S.prod g1 ∣ S.prod g2
theorem
Finset.prod_dvd_prod_of_subset
{ι : Type u_6}
{M : Type u_7}
[CommMonoid M]
(s t : Finset ι)
(f : ι → M)
(h : s ⊆ t)
:
∏ i ∈ s, f i ∣ ∏ i ∈ t, f i
theorem
Finset.isSquare_prod
{ι : Type u_1}
{α : Type u_3}
{s : Finset ι}
[CommMonoid α]
(f : ι → α)
(h : ∀ c ∈ s, IsSquare (f c))
:
IsSquare (∏ i ∈ s, f i)
theorem
Finset.even_sum
{ι : Type u_1}
{α : Type u_3}
{s : Finset ι}
[AddCommMonoid α]
(f : ι → α)
(h : ∀ c ∈ s, Even (f c))
:
Even (∑ i ∈ s, f i)
theorem
Finset.prod_sdiff_eq_prod_sdiff_iff
{ι : Type u_1}
{α : Type u_3}
[DecidableEq ι]
[CancelCommMonoid α]
{s t : Finset ι}
{f : ι → α}
:
theorem
Finset.sum_sdiff_eq_sum_sdiff_iff
{ι : Type u_1}
{α : Type u_3}
[DecidableEq ι]
[AddCancelCommMonoid α]
{s t : Finset ι}
{f : ι → α}
:
theorem
Finset.prod_sdiff_ne_prod_sdiff_iff
{ι : Type u_1}
{α : Type u_3}
[DecidableEq ι]
[CancelCommMonoid α]
{s t : Finset ι}
{f : ι → α}
:
theorem
Finset.sum_sdiff_ne_sum_sdiff_iff
{ι : Type u_1}
{α : Type u_3}
[DecidableEq ι]
[AddCancelCommMonoid α]
{s t : Finset ι}
{f : ι → α}
:
theorem
Finset.sum_card_fiberwise_eq_card_filter
{ι : Type u_1}
{κ : Type u_6}
[DecidableEq κ]
(s : Finset ι)
(t : Finset κ)
(g : ι → κ)
:
∑ j ∈ t, (Finset.filter (fun (i : ι) => g i = j) s).card = (Finset.filter (fun (i : ι) => g i ∈ t) s).card
theorem
Finset.card_filter
{ι : Type u_1}
(p : ι → Prop)
[DecidablePred p]
(s : Finset ι)
:
(Finset.filter (fun (i : ι) => p i) s).card = ∑ i ∈ s, if p i then 1 else 0
@[simp]
theorem
Finset.op_sum
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
{s : Finset α}
(f : α → β)
:
MulOpposite.op (∑ x ∈ s, f x) = ∑ x ∈ s, MulOpposite.op (f x)
Moving to the opposite additive commutative monoid commutes with summing.
@[simp]
theorem
Finset.unop_sum
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
{s : Finset α}
(f : α → βᵐᵒᵖ)
:
MulOpposite.unop (∑ x ∈ s, f x) = ∑ x ∈ s, MulOpposite.unop (f x)
@[simp]
theorem
Finset.prod_inv_distrib
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[DivisionCommMonoid β]
:
@[simp]
theorem
Finset.sum_neg_distrib
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[SubtractionCommMonoid β]
:
@[simp]
theorem
Finset.prod_div_distrib
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f g : α → β}
[DivisionCommMonoid β]
:
@[simp]
theorem
Finset.sum_sub_distrib
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f g : α → β}
[SubtractionCommMonoid β]
:
theorem
Finset.prod_zpow
{α : Type u_3}
{β : Type u_4}
[DivisionCommMonoid β]
(f : α → β)
(s : Finset α)
(n : ℤ)
:
theorem
Finset.sum_zsmul
{α : Type u_3}
{β : Type u_4}
[SubtractionCommMonoid β]
(f : α → β)
(s : Finset α)
(n : ℤ)
:
@[simp]
theorem
Finset.sum_sdiff_eq_sub
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[AddCommGroup β]
[DecidableEq α]
(h : s₁ ⊆ s₂)
:
theorem
Finset.sum_sdiff_sub_sum_sdiff
{α : Type u_3}
{β : Type u_4}
{s₁ s₂ : Finset α}
{f : α → β}
[AddCommGroup β]
[DecidableEq α]
:
@[simp]
theorem
Finset.prod_erase_eq_div
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommGroup β]
[DecidableEq α]
{a : α}
(h : a ∈ s)
:
@[simp]
theorem
Finset.sum_erase_eq_sub
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommGroup β]
[DecidableEq α]
{a : α}
(h : a ∈ s)
:
theorem
Finset.card_biUnion
{α : Type u_3}
{β : Type u_4}
[DecidableEq β]
{s : Finset α}
{t : α → Finset β}
(h : ∀ x ∈ s, ∀ y ∈ s, x ≠ y → Disjoint (t x) (t y))
:
(s.biUnion t).card = ∑ u ∈ s, (t u).card
theorem
Finset.card_biUnion_le
{α : Type u_3}
{β : Type u_4}
[DecidableEq β]
{s : Finset α}
{t : α → Finset β}
:
(s.biUnion t).card ≤ ∑ a ∈ s, (t a).card
theorem
Finset.card_eq_sum_card_fiberwise
{α : Type u_3}
{β : Type u_4}
[DecidableEq β]
{f : α → β}
{s : Finset α}
{t : Finset β}
(H : ∀ x ∈ s, f x ∈ t)
:
s.card = ∑ b ∈ t, (Finset.filter (fun (a : α) => f a = b) s).card
theorem
Finset.card_eq_sum_card_image
{α : Type u_3}
{β : Type u_4}
[DecidableEq β]
(f : α → β)
(s : Finset α)
:
s.card = ∑ b ∈ Finset.image f s, (Finset.filter (fun (a : α) => f a = b) s).card
theorem
Finset.prod_unique_nonempty
{α : Type u_6}
{β : Type u_7}
[CommMonoid β]
[Unique α]
(s : Finset α)
(f : α → β)
(h : s.Nonempty)
:
∏ x ∈ s, f x = f default
theorem
Finset.sum_unique_nonempty
{α : Type u_6}
{β : Type u_7}
[AddCommMonoid β]
[Unique α]
(s : Finset α)
(f : α → β)
(h : s.Nonempty)
:
∑ x ∈ s, f x = f default
theorem
Fintype.prod_bijective
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[CommMonoid α]
(e : ι → κ)
(he : Function.Bijective e)
(f : ι → α)
(g : κ → α)
(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.sum_bijective
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[AddCommMonoid α]
(e : ι → κ)
(he : Function.Bijective e)
(f : ι → α)
(g : κ → α)
(h : ∀ (x : ι), f x = g (e x))
:
∑ x : ι, f x = ∑ x : κ, g x
Fintype.sum_bijective is a variant of Finset.sum_bij that accepts
Function.Bijective.
See Function.Bijective.sum_comp for a version without h.
theorem
Function.Bijective.finset_prod
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[CommMonoid α]
(e : ι → κ)
(he : Function.Bijective e)
(f : ι → α)
(g : κ → α)
(h : ∀ (x : ι), f x = g (e x))
:
∏ x : ι, f x = ∏ x : κ, g x
Alias of Fintype.prod_bijective.
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
Function.Bijective.finset_sum
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[AddCommMonoid α]
(e : ι → κ)
(he : Function.Bijective e)
(f : ι → α)
(g : κ → α)
(h : ∀ (x : ι), f x = g (e x))
:
∑ x : ι, f x = ∑ x : κ, g x
theorem
Fintype.prod_equiv
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[CommMonoid α]
(e : ι ≃ κ)
(f : ι → α)
(g : κ → α)
(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_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[AddCommMonoid α]
(e : ι ≃ κ)
(f : ι → α)
(g : κ → α)
(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
Function.Bijective.prod_comp
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[CommMonoid α]
{e : ι → κ}
(he : Function.Bijective e)
(g : κ → α)
:
∏ i : ι, g (e i) = ∏ i : κ, g i
theorem
Function.Bijective.sum_comp
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[AddCommMonoid α]
{e : ι → κ}
(he : Function.Bijective e)
(g : κ → α)
:
∑ i : ι, g (e i) = ∑ i : κ, g i
theorem
Equiv.prod_comp
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[CommMonoid α]
(e : ι ≃ κ)
(g : κ → α)
:
∏ i : ι, g (e i) = ∏ i : κ, g i
theorem
Equiv.sum_comp
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[AddCommMonoid α]
(e : ι ≃ κ)
(g : κ → α)
:
∑ i : ι, g (e i) = ∑ i : κ, g i
theorem
Fintype.prod_of_injective
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[CommMonoid α]
(e : ι → κ)
(he : Function.Injective e)
(f : ι → α)
(g : κ → α)
(h' : ∀ i ∉ Set.range e, g i = 1)
(h : ∀ (i : ι), f i = g (e i))
:
∏ i : ι, f i = ∏ j : κ, g j
theorem
Fintype.sum_of_injective
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[AddCommMonoid α]
(e : ι → κ)
(he : Function.Injective e)
(f : ι → α)
(g : κ → α)
(h' : ∀ i ∉ Set.range e, g i = 0)
(h : ∀ (i : ι), f i = g (e i))
:
∑ i : ι, f i = ∑ j : κ, g j
theorem
Fintype.prod_fiberwise
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[CommMonoid α]
[DecidableEq κ]
(g : ι → κ)
(f : ι → α)
:
theorem
Fintype.sum_fiberwise
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[AddCommMonoid α]
[DecidableEq κ]
(g : ι → κ)
(f : ι → α)
:
theorem
Fintype.prod_fiberwise'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[CommMonoid α]
[DecidableEq κ]
(g : ι → κ)
(f : κ → α)
:
theorem
Fintype.sum_fiberwise'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[Fintype ι]
[Fintype κ]
[AddCommMonoid α]
[DecidableEq κ]
(g : ι → κ)
(f : κ → α)
:
theorem
Fintype.prod_unique
{α : Type u_9}
{β : Type u_10}
[CommMonoid β]
[Unique α]
[Fintype α]
(f : α → β)
:
∏ x : α, f x = f default
theorem
Fintype.sum_unique
{α : Type u_9}
{β : Type u_10}
[AddCommMonoid β]
[Unique α]
[Fintype α]
(f : α → β)
:
∑ x : α, f x = f default
theorem
Fintype.prod_empty
{α : Type u_9}
{β : Type u_10}
[CommMonoid β]
[IsEmpty α]
[Fintype α]
(f : α → β)
:
∏ x : α, f x = 1
theorem
Fintype.sum_empty
{α : Type u_9}
{β : Type u_10}
[AddCommMonoid β]
[IsEmpty α]
[Fintype α]
(f : α → β)
:
∑ x : α, f x = 0
theorem
Fintype.prod_subsingleton
{α : Type u_9}
{β : Type u_10}
[CommMonoid β]
[Subsingleton α]
[Fintype α]
(f : α → β)
(a : α)
:
∏ x : α, f x = f a
theorem
Fintype.sum_subsingleton
{α : Type u_9}
{β : Type u_10}
[AddCommMonoid β]
[Subsingleton α]
[Fintype α]
(f : α → β)
(a : α)
:
∑ x : α, f x = f a
theorem
Fintype.prod_subtype_mul_prod_subtype
{α : Type u_9}
{β : Type u_10}
[Fintype α]
[CommMonoid β]
(p : α → Prop)
(f : α → β)
[DecidablePred p]
:
theorem
Fintype.sum_subtype_add_sum_subtype
{α : Type u_9}
{β : Type u_10}
[Fintype α]
[AddCommMonoid β]
(p : α → Prop)
(f : α → β)
[DecidablePred p]
:
theorem
Fintype.prod_subset
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[CommMonoid α]
{s : Finset ι}
{f : ι → α}
(h : ∀ (i : ι), f i ≠ 1 → i ∈ s)
:
∏ i ∈ s, f i = ∏ i : ι, f i
theorem
Fintype.sum_subset
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[AddCommMonoid α]
{s : Finset ι}
{f : ι → α}
(h : ∀ (i : ι), f i ≠ 0 → i ∈ s)
:
∑ i ∈ s, f i = ∑ i : ι, f i
theorem
Fintype.prod_ite_eq_ite_exists
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[CommMonoid α]
(p : ι → Prop)
[DecidablePred p]
(h : ∀ (i j : ι), p i → p j → i = j)
(a : α)
:
(∏ i : ι, if p i then a else 1) = if ∃ (i : ι), p i then a else 1
theorem
Fintype.sum_ite_eq_ite_exists
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[AddCommMonoid α]
(p : ι → Prop)
[DecidablePred p]
(h : ∀ (i j : ι), p i → p j → i = j)
(a : α)
:
(∑ i : ι, if p i then a else 0) = if ∃ (i : ι), p i then a else 0
theorem
Fintype.prod_ite_mem
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[CommMonoid α]
[DecidableEq ι]
(s : Finset ι)
(f : ι → α)
:
theorem
Fintype.sum_ite_mem
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[AddCommMonoid α]
[DecidableEq ι]
(s : Finset ι)
(f : ι → α)
:
theorem
Fintype.prod_dite_eq
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[CommMonoid α]
[DecidableEq ι]
(i : ι)
(f : (j : ι) → i = j → α)
:
See also Finset.prod_dite_eq.
theorem
Fintype.sum_dite_eq
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[AddCommMonoid α]
[DecidableEq ι]
(i : ι)
(f : (j : ι) → i = j → α)
:
See also Finset.sum_dite_eq.
theorem
Fintype.prod_dite_eq'
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[CommMonoid α]
[DecidableEq ι]
(i : ι)
(f : (j : ι) → j = i → α)
:
See also Finset.prod_dite_eq'.
theorem
Fintype.sum_dite_eq'
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[AddCommMonoid α]
[DecidableEq ι]
(i : ι)
(f : (j : ι) → j = i → α)
:
See also Finset.sum_dite_eq'.
theorem
Fintype.prod_ite_eq
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[CommMonoid α]
[DecidableEq ι]
(i : ι)
(f : ι → α)
:
See also Finset.prod_ite_eq.
theorem
Fintype.sum_ite_eq
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[AddCommMonoid α]
[DecidableEq ι]
(i : ι)
(f : ι → α)
:
See also Finset.sum_ite_eq.
theorem
Fintype.prod_ite_eq'
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[CommMonoid α]
[DecidableEq ι]
(i : ι)
(f : ι → α)
:
See also Finset.prod_ite_eq'.
theorem
Fintype.sum_ite_eq'
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[AddCommMonoid α]
[DecidableEq ι]
(i : ι)
(f : ι → α)
:
See also Finset.sum_ite_eq'.
theorem
Fintype.prod_pi_mulSingle
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
{α : ι → Type u_9}
[(i : ι) → CommMonoid (α i)]
(i : ι)
(f : (i : ι) → α i)
:
∏ j : ι, Pi.mulSingle j (f j) i = f i
See also Finset.prod_pi_mulSingle.
theorem
Fintype.sum_pi_single
{ι : Type u_6}
[Fintype ι]
[DecidableEq ι]
{α : ι → Type u_9}
[(i : ι) → AddCommMonoid (α i)]
(i : ι)
(f : (i : ι) → α i)
:
See also Finset.sum_pi_single.
theorem
Fintype.prod_pi_mulSingle'
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[CommMonoid α]
[DecidableEq ι]
(i : ι)
(a : α)
:
∏ j : ι, Pi.mulSingle i a j = a
See also Finset.prod_pi_mulSingle'.
theorem
Fintype.sum_pi_single'
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[AddCommMonoid α]
[DecidableEq ι]
(i : ι)
(a : α)
:
See also Finset.sum_pi_single'.
@[simp]
theorem
Finset.prod_attach_univ
{ι : Type u_1}
{α : Type u_3}
[CommMonoid α]
[Fintype ι]
(f : { i : ι // i ∈ Finset.univ } → α)
:
∏ i ∈ Finset.univ.attach, f i = ∏ i : ι, f ⟨i, ⋯⟩
@[simp]
theorem
Finset.sum_attach_univ
{ι : Type u_1}
{α : Type u_3}
[AddCommMonoid α]
[Fintype ι]
(f : { i : ι // i ∈ Finset.univ } → α)
:
∑ i ∈ Finset.univ.attach, f i = ∑ i : ι, f ⟨i, ⋯⟩
theorem
Finset.prod_erase_attach
{ι : Type u_1}
{α : Type u_3}
[CommMonoid α]
[DecidableEq ι]
{s : Finset ι}
(f : ι → α)
(i : { x : ι // x ∈ s })
:
∏ j ∈ s.attach.erase i, f ↑j = ∏ j ∈ s.erase ↑i, f j
theorem
Finset.sum_erase_attach
{ι : Type u_1}
{α : Type u_3}
[AddCommMonoid α]
[DecidableEq ι]
{s : Finset ι}
(f : ι → α)
(i : { x : ι // x ∈ s })
:
∑ j ∈ s.attach.erase i, f ↑j = ∑ j ∈ s.erase ↑i, f j
theorem
List.prod_toFinset
{α : Type u_3}
{M : Type u_6}
[DecidableEq α]
[CommMonoid M]
(f : α → M)
{l : List α}
(_hl : l.Nodup)
:
theorem
List.sum_toFinset
{α : Type u_3}
{M : Type u_6}
[DecidableEq α]
[AddCommMonoid M]
(f : α → M)
{l : List α}
(_hl : l.Nodup)
:
@[simp]
theorem
List.sum_toFinset_count_eq_length
{α : Type u_3}
[DecidableEq α]
(l : List α)
:
∑ a ∈ l.toFinset, List.count a l = l.length
theorem
Multiset.toFinset_sum_count_eq
{α : Type u_3}
[DecidableEq α]
(s : Multiset α)
:
∑ a ∈ s.toFinset, Multiset.count a s = s.card
@[simp]
theorem
Multiset.sum_count_eq_card
{α : Type u_3}
[DecidableEq α]
{s : Finset α}
{m : Multiset α}
(hms : ∀ a ∈ m, a ∈ s)
:
∑ a ∈ s, Multiset.count a m = m.card
@[deprecated Multiset.sum_count_eq_card]
theorem
Multiset.sum_count_eq
{α : Type u_3}
[DecidableEq α]
[Fintype α]
(s : Multiset α)
:
∑ a : α, Multiset.count a s = s.card
theorem
Multiset.count_sum'
{α : Type u_3}
{β : Type u_4}
[DecidableEq α]
{s : Finset β}
{a : α}
{f : β → Multiset α}
:
Multiset.count a (∑ x ∈ s, f x) = ∑ x ∈ s, Multiset.count a (f x)
@[simp]
theorem
Multiset.toFinset_sum_count_nsmul_eq
{α : Type u_3}
[DecidableEq α]
(s : Multiset α)
:
∑ a ∈ s.toFinset, Multiset.count a s • {a} = s
theorem
Multiset.exists_smul_of_dvd_count
{α : Type u_3}
[DecidableEq α]
(s : Multiset α)
{k : ℕ}
(h : ∀ a ∈ s, k ∣ Multiset.count a s)
:
theorem
Multiset.toFinset_prod_dvd_prod
{α : Type u_3}
[DecidableEq α]
[CommMonoid α]
(S : Multiset α)
:
S.toFinset.prod id ∣ S.prod
theorem
Multiset.prod_sum
{α : Type u_6}
{ι : Type u_7}
[CommMonoid α]
(f : ι → Multiset α)
(s : Finset ι)
:
(∑ x ∈ s, f x).prod = ∏ x ∈ s, (f x).prod
theorem
Multiset.sum_sum
{α : Type u_6}
{ι : Type u_7}
[AddCommMonoid α]
(f : ι → Multiset α)
(s : Finset ι)
:
(∑ x ∈ s, f x).sum = ∑ x ∈ s, (f x).sum
@[simp]
theorem
Units.coe_prod
{α : Type u_3}
{M : Type u_6}
[CommMonoid M]
(f : α → Mˣ)
(s : Finset α)
:
↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
@[simp]
@[simp]
theorem
IsAddUnit.sum_iff
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
:
theorem
IsAddUnit.sum_univ_iff
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[Fintype α]
[AddCommMonoid β]
:
@[simp]
@[simp]
theorem
ofMul_multiset_prod
{α : Type u_3}
[CommMonoid α]
(s : Multiset α)
:
Additive.ofMul s.prod = (Multiset.map (⇑Additive.ofMul) s).sum
@[simp]
theorem
toMul_multiset_sum
{α : Type u_3}
[CommMonoid α]
(s : Multiset (Additive α))
:
Additive.toMul s.sum = (Multiset.map (⇑Additive.toMul) s).prod
@[simp]
theorem
ofMul_prod
{ι : Type u_1}
{α : Type u_3}
[CommMonoid α]
(s : Finset ι)
(f : ι → α)
:
Additive.ofMul (∏ i ∈ s, f i) = ∑ i ∈ s, Additive.ofMul (f i)
@[simp]
theorem
ofAdd_multiset_prod
{α : Type u_3}
[AddCommMonoid α]
(s : Multiset α)
:
Multiplicative.ofAdd s.sum = (Multiset.map (⇑Multiplicative.ofAdd) s).prod
@[simp]
theorem
toAdd_multiset_sum
{α : Type u_3}
[AddCommMonoid α]
(s : Multiset (Multiplicative α))
:
Multiplicative.toAdd s.prod = (Multiset.map (⇑Multiplicative.toAdd) s).sum
@[simp]
theorem
toAdd_prod
{ι : Type u_1}
{α : Type u_3}
[AddCommMonoid α]
(s : Finset ι)
(f : ι → Multiplicative α)
:
Multiplicative.toAdd (∏ i ∈ s, f i) = ∑ i ∈ s, Multiplicative.toAdd (f i)