theorem
Finset.prod_eq_fold
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
(s : Finset ι)
(f : ι → M)
:
theorem
Finset.sum_eq_fold
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
(s : Finset ι)
(f : ι → M)
:
@[simp]
theorem
Finset.prod_cons
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
{a : ι}
[CommMonoid M]
{f : ι → M}
(h : a ∉ s)
:
@[simp]
theorem
Finset.sum_cons
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
{a : ι}
[AddCommMonoid M]
{f : ι → M}
(h : a ∉ s)
:
theorem
Finset.sum_cons'
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
{a : ι}
[AddCommMonoid M]
(h : a ∉ s)
:
@[simp]
theorem
Finset.prod_insert
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
{a : ι}
[CommMonoid M]
{f : ι → M}
[DecidableEq ι]
:
@[simp]
theorem
Finset.sum_insert
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
{a : ι}
[AddCommMonoid M]
{f : ι → M}
[DecidableEq ι]
:
theorem
Finset.prod_insert'
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
{a : ι}
[CommMonoid M]
[DecidableEq ι]
(h : a ∉ s)
:
Variant of prod_insert not applied to a function.
theorem
Finset.sum_insert'
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
{a : ι}
[AddCommMonoid M]
[DecidableEq ι]
(h : a ∉ s)
:
@[simp]
theorem
Finset.prod_insert_of_eq_one_if_notMem
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
{a : ι}
[CommMonoid M]
{f : ι → M}
[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_notMem
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
{a : ι}
[AddCommMonoid M]
{f : ι → M}
[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.
theorem
Finset.prod_insert_one
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
{a : ι}
[CommMonoid M]
{f : ι → M}
[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.
theorem
Finset.sum_insert_zero
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
{a : ι}
[AddCommMonoid M]
{f : ι → M}
[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.
@[simp]
@[simp]
Variant of prod_singleton not applied to a function.
theorem
Finset.prod_pair
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
{f : ι → M}
[DecidableEq ι]
{a b : ι}
(h : a ≠ b)
:
theorem
Finset.sum_pair
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
{f : ι → M}
[DecidableEq ι]
{a b : ι}
(h : a ≠ b)
:
@[simp]
theorem
Finset.prod_image
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
{f : ι → M}
[DecidableEq ι]
{s : Finset κ}
{g : κ → ι}
:
If a function is injective on a finset, products over the original finset or its image coincide.
See also prod_image_of_pairwise_eq_one for a version with weaker assumptions.
@[simp]
theorem
Finset.sum_image
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
{f : ι → M}
[DecidableEq ι]
{s : Finset κ}
{g : κ → ι}
:
If a function is injective on a finset, sums over the original
finset or its image coincide.
See also sum_image_of_pairwise_eq_zero for a version with weaker assumptions.
theorem
Finset.prod_attach
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
(s : Finset ι)
(f : ι → M)
:
theorem
Finset.sum_attach
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
(s : Finset ι)
(f : ι → M)
:
theorem
Finset.prod_eq_one
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
{f : ι → M}
(h : ∀ x ∈ s, f x = 1)
:
theorem
Finset.sum_eq_zero
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
{f : ι → M}
(h : ∀ x ∈ s, f x = 0)
:
@[simp]
theorem
Finset.prod_eq_one_iff
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
{f : ι → M}
[Subsingleton Mˣ]
:
In a monoid whose only unit is 1, a product is equal to 1 iff all factors are 1.
@[simp]
theorem
Finset.sum_eq_zero_iff
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
{f : ι → M}
[Subsingleton (AddUnits M)]
:
In an additive monoid whose only unit is 0, a sum is equal to 0 iff all terms are 0.
theorem
Finset.prod_disjUnion
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[CommMonoid M]
{f : ι → M}
(h : Disjoint s₁ s₂)
:
theorem
Finset.sum_disjUnion
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[AddCommMonoid M]
{f : ι → M}
(h : Disjoint s₁ s₂)
:
theorem
Finset.prod_disjiUnion
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
{f : ι → M}
(s : Finset κ)
(t : κ → Finset ι)
(h : (↑s).PairwiseDisjoint t)
:
theorem
Finset.sum_disjiUnion
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
{f : ι → M}
(s : Finset κ)
(t : κ → Finset ι)
(h : (↑s).PairwiseDisjoint t)
:
theorem
Finset.prod_union_inter
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[CommMonoid M]
{f : ι → M}
[DecidableEq ι]
:
theorem
Finset.sum_union_inter
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[AddCommMonoid M]
{f : ι → M}
[DecidableEq ι]
:
theorem
Finset.prod_union
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[CommMonoid M]
{f : ι → M}
[DecidableEq ι]
(h : Disjoint s₁ s₂)
:
theorem
Finset.sum_union
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[AddCommMonoid M]
{f : ι → M}
[DecidableEq ι]
(h : Disjoint s₁ s₂)
:
theorem
Finset.prod_filter_mul_prod_filter_not
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
(s : Finset ι)
(p : ι → Prop)
[DecidablePred p]
[(x : ι) → Decidable ¬p x]
(f : ι → M)
:
theorem
Finset.sum_filter_add_sum_filter_not
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
(s : Finset ι)
(p : ι → Prop)
[DecidablePred p]
[(x : ι) → Decidable ¬p x]
(f : ι → M)
:
theorem
Finset.prod_filter_not_mul_prod_filter
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
(s : Finset ι)
(p : ι → Prop)
[DecidablePred p]
[(x : ι) → Decidable ¬p x]
(f : ι → M)
:
theorem
Finset.sum_filter_not_add_sum_filter
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
(s : Finset ι)
(p : ι → Prop)
[DecidablePred p]
[(x : ι) → Decidable ¬p x]
(f : ι → M)
:
theorem
Finset.prod_filter_xor
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
{f : ι → M}
(p q : ι → Prop)
[DecidablePred p]
[DecidablePred q]
:
theorem
Finset.sum_filter_xor
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
{f : ι → M}
(p q : ι → Prop)
[DecidablePred p]
[DecidablePred q]
:
theorem
IsCompl.prod_mul_prod
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
[Fintype ι]
{s t : Finset ι}
(h : IsCompl s t)
(f : ι → M)
:
theorem
IsCompl.sum_add_sum
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
[Fintype ι]
{s t : Finset ι}
(h : IsCompl s t)
(f : ι → M)
:
theorem
Finset.prod_mul_prod_compl
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
[Fintype ι]
[DecidableEq ι]
(s : Finset ι)
(f : ι → M)
:
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_1}
{M : Type u_4}
[AddCommMonoid M]
[Fintype ι]
[DecidableEq ι]
(s : Finset ι)
(f : ι → M)
:
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_1}
{M : Type u_4}
[CommMonoid M]
[Fintype ι]
[DecidableEq ι]
(s : Finset ι)
(f : ι → M)
:
theorem
Finset.sum_compl_add_sum
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
[Fintype ι]
[DecidableEq ι]
(s : Finset ι)
(f : ι → M)
:
theorem
Finset.prod_sdiff
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[CommMonoid M]
{f : ι → M}
[DecidableEq ι]
(h : s₁ ⊆ s₂)
:
theorem
Finset.sum_sdiff
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[AddCommMonoid M]
{f : ι → M}
[DecidableEq ι]
(h : s₁ ⊆ s₂)
:
theorem
Finset.prod_subset_one_on_sdiff
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[CommMonoid M]
{f g : ι → M}
[DecidableEq ι]
(h : s₁ ⊆ s₂)
(hg : ∀ x ∈ s₂ \ s₁, g x = 1)
(hfg : ∀ x ∈ s₁, f x = g x)
:
theorem
Finset.sum_subset_zero_on_sdiff
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[AddCommMonoid M]
{f g : ι → M}
[DecidableEq ι]
(h : s₁ ⊆ s₂)
(hg : ∀ x ∈ s₂ \ s₁, g x = 0)
(hfg : ∀ x ∈ s₁, f x = g x)
:
theorem
Finset.prod_subset
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[CommMonoid M]
{f : ι → M}
(h : s₁ ⊆ s₂)
(hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 1)
:
theorem
Finset.sum_subset
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[AddCommMonoid M]
{f : ι → M}
(h : s₁ ⊆ s₂)
(hf : ∀ x ∈ s₂, x ∉ s₁ → f x = 0)
:
theorem
Finset.prod_biUnion
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
{f : ι → M}
[DecidableEq ι]
{s : Finset κ}
{t : κ → Finset ι}
(hs : (↑s).PairwiseDisjoint t)
:
Given a finite family of pairwise disjoint finsets, the product over their union is the product
of the products over the sets.
See also prod_biUnion_of_pairwise_eq_one for a version with weaker assumptions.
theorem
Finset.sum_biUnion
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
{f : ι → M}
[DecidableEq ι]
{s : Finset κ}
{t : κ → Finset ι}
(hs : (↑s).PairwiseDisjoint t)
:
Given a finite family of pairwise disjoint finsets, the sum over their union is
the sum of the sums over the sets.
See also sum_biUnion_of_pairwise_eq_zero for a version with weaker assumptions.
theorem
Finset.prod_of_injOn
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
{s : Finset ι}
{t : Finset κ}
{f : ι → M}
{g : κ → M}
(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))
:
theorem
Finset.sum_of_injOn
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
{s : Finset ι}
{t : Finset κ}
{f : ι → M}
{g : κ → M}
(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))
:
theorem
Finset.prod_fiberwise_eq_prod_filter
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
[DecidableEq κ]
(s : Finset ι)
(t : Finset κ)
(g : ι → κ)
(f : ι → M)
:
theorem
Finset.sum_fiberwise_eq_sum_filter
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq κ]
(s : Finset ι)
(t : Finset κ)
(g : ι → κ)
(f : ι → M)
:
theorem
Finset.prod_fiberwise_eq_prod_filter'
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
[DecidableEq κ]
(s : Finset ι)
(t : Finset κ)
(g : ι → κ)
(f : κ → M)
:
theorem
Finset.sum_fiberwise_eq_sum_filter'
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq κ]
(s : Finset ι)
(t : Finset κ)
(g : ι → κ)
(f : κ → M)
:
theorem
Finset.prod_fiberwise_of_maps_to
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
{s : Finset ι}
{t : Finset κ}
[DecidableEq κ]
{g : ι → κ}
(h : ∀ i ∈ s, g i ∈ t)
(f : ι → M)
:
theorem
Finset.sum_fiberwise_of_maps_to
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
{s : Finset ι}
{t : Finset κ}
[DecidableEq κ]
{g : ι → κ}
(h : ∀ i ∈ s, g i ∈ t)
(f : ι → M)
:
theorem
Finset.prod_fiberwise_of_maps_to'
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
{s : Finset ι}
{t : Finset κ}
[DecidableEq κ]
{g : ι → κ}
(h : ∀ i ∈ s, g i ∈ t)
(f : κ → M)
:
theorem
Finset.sum_fiberwise_of_maps_to'
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
{s : Finset ι}
{t : Finset κ}
[DecidableEq κ]
{g : ι → κ}
(h : ∀ i ∈ s, g i ∈ t)
(f : κ → M)
:
theorem
Finset.prod_fiberwise
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
[DecidableEq κ]
[Fintype κ]
(s : Finset ι)
(g : ι → κ)
(f : ι → M)
:
theorem
Finset.sum_fiberwise
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq κ]
[Fintype κ]
(s : Finset ι)
(g : ι → κ)
(f : ι → M)
:
theorem
Finset.prod_fiberwise'
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
[DecidableEq κ]
[Fintype κ]
(s : Finset ι)
(g : ι → κ)
(f : κ → M)
:
theorem
Finset.sum_fiberwise'
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq κ]
[Fintype κ]
(s : Finset ι)
(g : ι → κ)
(f : κ → M)
:
theorem
Finset.prod_image'
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
{f : ι → M}
[DecidableEq ι]
{s : Finset κ}
{g : κ → ι}
(h : κ → M)
(eq : ∀ i ∈ s, f (g i) = ∏ j ∈ s with g j = g i, h j)
:
theorem
Finset.sum_image'
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
{f : ι → M}
[DecidableEq ι]
{s : Finset κ}
{g : κ → ι}
(h : κ → M)
(eq : ∀ i ∈ s, f (g i) = ∑ j ∈ s with g j = g i, h j)
:
theorem
Finset.prod_mul_distrib
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
{f g : ι → M}
:
theorem
Finset.sum_add_distrib
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
{f g : ι → M}
:
theorem
Finset.prod_filter_of_ne
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
{f : ι → M}
{p : ι → Prop}
[DecidablePred p]
(hp : ∀ x ∈ s, f x ≠ 1 → p x)
:
theorem
Finset.sum_filter_of_ne
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
{f : ι → M}
{p : ι → Prop}
[DecidablePred p]
(hp : ∀ x ∈ s, f x ≠ 0 → p x)
:
theorem
Finset.prod_filter_ne_one
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
{f : ι → M}
(s : Finset ι)
[(x : ι) → Decidable (f x ≠ 1)]
:
theorem
Finset.sum_filter_ne_zero
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
{f : ι → M}
(s : Finset ι)
[(x : ι) → Decidable (f x ≠ 0)]
:
theorem
Finset.prod_filter
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
(p : ι → Prop)
[DecidablePred p]
(f : ι → M)
:
theorem
Finset.sum_filter
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
(p : ι → Prop)
[DecidablePred p]
(f : ι → M)
:
theorem
Finset.prod_eq_single_of_mem
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
{s : Finset ι}
{f : ι → M}
(a : ι)
(h : a ∈ s)
(h₀ : ∀ b ∈ s, b ≠ a → f b = 1)
:
theorem
Finset.sum_eq_single_of_mem
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
{s : Finset ι}
{f : ι → M}
(a : ι)
(h : a ∈ s)
(h₀ : ∀ b ∈ s, b ≠ a → f b = 0)
:
theorem
Finset.prod_eq_single
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
{s : Finset ι}
{f : ι → M}
(a : ι)
(h₀ : ∀ b ∈ s, b ≠ a → f b = 1)
(h₁ : a ∉ s → f a = 1)
:
theorem
Finset.sum_eq_single
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
{s : Finset ι}
{f : ι → M}
(a : ι)
(h₀ : ∀ b ∈ s, b ≠ a → f b = 0)
(h₁ : a ∉ s → f a = 0)
:
@[simp]
theorem
Finset.prod_ite_mem_eq
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
[Fintype ι]
(s : Finset ι)
(f : ι → M)
[DecidablePred fun (x : ι) => x ∈ s]
:
@[simp]
theorem
Finset.sum_ite_mem_eq
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
[Fintype ι]
(s : Finset ι)
(f : ι → M)
[DecidablePred fun (x : ι) => x ∈ s]
:
theorem
Finset.prod_eq_ite
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
[DecidableEq ι]
{s : Finset ι}
{f : ι → M}
(a : ι)
(h₀ : ∀ b ∈ s, b ≠ a → f b = 1)
:
theorem
Finset.sum_eq_ite
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq ι]
{s : Finset ι}
{f : ι → M}
(a : ι)
(h₀ : ∀ b ∈ s, b ≠ a → f b = 0)
:
theorem
Finset.prod_union_eq_left
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[CommMonoid M]
{f : ι → M}
[DecidableEq ι]
(hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 1)
:
theorem
Finset.sum_union_eq_left
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[AddCommMonoid M]
{f : ι → M}
[DecidableEq ι]
(hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 0)
:
theorem
Finset.prod_union_eq_right
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[CommMonoid M]
{f : ι → M}
[DecidableEq ι]
(hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1)
:
theorem
Finset.sum_union_eq_right
{ι : Type u_1}
{M : Type u_4}
{s₁ s₂ : Finset ι}
[AddCommMonoid M]
{f : ι → M}
[DecidableEq ι]
(hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 0)
:
theorem
Finset.prod_congr_of_eq_on_inter
{ι : Type u_5}
{M : Type u_6}
{s₁ s₂ : Finset ι}
{f g : ι → M}
[CommMonoid M]
(h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1)
(h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1)
(h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a)
:
The products of two functions f g : ι → M over finite sets s₁ s₂ : Finset ι
are equal if the functions agree on s₁ ∩ s₂, f = 1 and g = 1 on the respective
set differences.
theorem
Finset.sum_congr_of_eq_on_inter
{ι : Type u_5}
{M : Type u_6}
{s₁ s₂ : Finset ι}
{f g : ι → M}
[AddCommMonoid M]
(h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 0)
(h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 0)
(h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a)
:
The sum of two functions f g : ι → M over finite sets s₁ s₂ : Finset ι
are equal if the functions agree on s₁ ∩ s₂, f = 0 and g = 0 on the respective
set differences.
@[simp]
theorem
Finset.prod_subtype_eq_prod_filter
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
(f : ι → M)
{p : ι → Prop}
[DecidablePred p]
:
A product over s.subtype p equals one over {x ∈ s | p x}.
@[simp]
theorem
Finset.sum_subtype_eq_sum_filter
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
(f : ι → M)
{p : ι → Prop}
[DecidablePred p]
:
A sum over s.subtype p equals one over {x ∈ s | p x}.
theorem
Finset.prod_subtype_of_mem
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
(f : ι → M)
{p : ι → Prop}
[DecidablePred p]
(h : ∀ x ∈ s, p 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_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
(f : ι → M)
{p : ι → Prop}
[DecidablePred p]
(h : ∀ x ∈ s, p 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_1}
{M : Type u_4}
[CommMonoid M]
{p : ι → Prop}
{s : Finset { x : ι // p x }}
{f : { x : ι // p x } → M}
{g : ι → M}
(h : ∀ x ∈ s, g ↑x = f x)
:
A product of a function over a Finset in a subtype equals a
product in the main type of a function that agrees with the first
function on that Finset.
theorem
Finset.sum_subtype_map_embedding
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
{p : ι → Prop}
{s : Finset { x : ι // p x }}
{f : { x : ι // p x } → M}
{g : ι → M}
(h : ∀ x ∈ s, g ↑x = f x)
:
A sum of a function over a Finset in a subtype equals a
sum in the main type of a function that agrees with the first
function on that Finset.
theorem
Finset.prod_coe_sort
{ι : Type u_1}
{M : Type u_4}
(s : Finset ι)
[CommMonoid M]
(f : ι → M)
:
theorem
Finset.sum_coe_sort
{ι : Type u_1}
{M : Type u_4}
(s : Finset ι)
[AddCommMonoid M]
(f : ι → M)
:
theorem
Finset.prod_finset_coe
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
(f : ι → M)
(s : Finset ι)
:
theorem
Finset.sum_finset_coe
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
(f : ι → M)
(s : Finset ι)
:
theorem
Finset.prod_set_coe
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
{f : ι → M}
(s : Set ι)
[Fintype ↑s]
:
theorem
Finset.sum_set_coe
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
{f : ι → M}
(s : Set ι)
[Fintype ↑s]
:
theorem
Finset.prod_congr_set
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
[Fintype ι]
(s : Set ι)
[DecidablePred fun (x : ι) => x ∈ s]
(f : ι → M)
(g : ↑s → M)
(w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩)
(w' : ∀ x ∉ s, f x = 1)
:
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_1}
{M : Type u_4}
[AddCommMonoid M]
[Fintype ι]
(s : Set ι)
[DecidablePred fun (x : ι) => x ∈ s]
(f : ι → M)
(g : ↑s → M)
(w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩)
(w' : ∀ x ∉ s, f x = 0)
:
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_extend_by_one
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
[DecidableEq ι]
(s : Finset ι)
(f : ι → M)
:
theorem
Finset.sum_extend_by_zero
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq ι]
(s : Finset ι)
(f : ι → M)
:
theorem
Finset.prod_eq_prod_extend
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
(f : ↥s → M)
:
Also see Finset.prod_ite_mem_eq
theorem
Finset.sum_eq_sum_extend
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
(f : ↥s → M)
:
Also see Finset.sum_ite_mem_eq
theorem
Finset.prod_bij_ne_one
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
{s : Finset ι}
{t : Finset κ}
{f : ι → M}
{g : κ → M}
(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₂))
:
theorem
Finset.sum_bij_ne_zero
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
{s : Finset ι}
{t : Finset κ}
{f : ι → M}
{g : κ → M}
(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₂))
:
theorem
Finset.exists_ne_one_of_prod_ne_one
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
{f : ι → M}
(h : ∏ x ∈ s, f x ≠ 1)
:
∃ a ∈ s, f a ≠ 1
theorem
Finset.exists_ne_zero_of_sum_ne_zero
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
{f : ι → M}
(h : ∑ x ∈ s, f x ≠ 0)
:
∃ a ∈ s, f a ≠ 0
theorem
Finset.prod_list_map_count
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
[DecidableEq ι]
(l : List ι)
(f : ι → M)
:
theorem
Finset.sum_list_map_count
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq ι]
(l : List ι)
(f : ι → M)
:
theorem
Finset.prod_list_count_of_subset
{M : Type u_4}
[CommMonoid M]
[DecidableEq M]
(m : List M)
(s : Finset M)
(hs : m.toFinset ⊆ s)
:
theorem
Finset.sum_list_count_of_subset
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq M]
(m : List M)
(s : Finset M)
(hs : m.toFinset ⊆ s)
:
theorem
Finset.prod_multiset_map_count
{ι : Type u_1}
[DecidableEq ι]
(s : Multiset ι)
{M : Type u_5}
[CommMonoid M]
(f : ι → M)
:
theorem
Finset.sum_multiset_map_count
{ι : Type u_1}
[DecidableEq ι]
(s : Multiset ι)
{M : Type u_5}
[AddCommMonoid M]
(f : ι → M)
:
theorem
Finset.sum_multiset_count
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq M]
(s : Multiset M)
:
theorem
Finset.prod_multiset_count_of_subset
{M : Type u_4}
[CommMonoid M]
[DecidableEq M]
(m : Multiset M)
(s : Finset M)
(hs : m.toFinset ⊆ s)
:
theorem
Finset.sum_multiset_count_of_subset
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq M]
(m : Multiset M)
(s : Finset M)
(hs : m.toFinset ⊆ s)
:
theorem
Finset.prod_range_induction
{M : Type u_4}
[CommMonoid M]
(f s : ℕ → M)
(base : s 0 = 1)
(n : ℕ)
(step : ∀ k < n, s (k + 1) = s k * f k)
:
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 up to n.
This is a multiplicative discrete analogue of the fundamental theorem of calculus.
theorem
Finset.sum_range_induction
{M : Type u_4}
[AddCommMonoid M]
(f s : ℕ → M)
(base : s 0 = 0)
(n : ℕ)
(step : ∀ k < n, s (k + 1) = s k + f k)
:
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
up to n.
This is a discrete analogue of the fundamental theorem of calculus.
@[simp]
@[simp]
theorem
Finset.prod_eq_pow_card
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
{f : ι → M}
{b : M}
(hf : ∀ a ∈ s, f a = b)
:
theorem
Finset.sum_eq_card_nsmul
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
{f : ι → M}
{b : M}
(hf : ∀ a ∈ s, f a = b)
:
theorem
Finset.prod_pow_eq_pow_sum
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
(s : Finset ι)
(f : ι → ℕ)
(a : M)
:
theorem
Finset.sum_nsmul_assoc
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
(s : Finset ι)
(f : ι → ℕ)
(a : M)
:
theorem
Finset.prod_involution
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
{f : ι → M}
(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)
:
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_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
{f : ι → M}
(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)
:
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_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
{f : ι → M}
(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)
:
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_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
{f : ι → M}
(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)
:
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_1}
{κ : Type u_2}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
[DecidableEq κ]
(f : κ → M)
(g : ι → κ)
:
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_1}
{κ : Type u_2}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
[DecidableEq κ]
(f : κ → M)
(g : ι → κ)
:
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_partition
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
{f : ι → M}
(R : Setoid ι)
[DecidableRel ⇑R]
:
A product can be partitioned into a product of products, each equivalent under a setoid.
theorem
Finset.sum_partition
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
{f : ι → M}
(R : Setoid ι)
[DecidableRel ⇑R]
:
A sum can be partitioned into a sum of sums, each equivalent under a setoid.
theorem
Finset.prod_cancels_of_partition_cancels
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
{f : ι → M}
(R : Setoid ι)
[DecidableRel ⇑R]
(h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 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_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
{f : ι → M}
(R : Setoid ι)
[DecidableRel ⇑R]
(h : ∀ x ∈ s, ∑ a ∈ s with R a x, f a = 0)
:
If we can partition a sum into subsets that cancel out, then the whole sum cancels.
theorem
Finset.mul_prod_erase
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
[DecidableEq ι]
(s : Finset ι)
(f : ι → M)
{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_1}
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq ι]
(s : Finset ι)
(f : ι → M)
{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_1}
{M : Type u_4}
[CommMonoid M]
[DecidableEq ι]
(s : Finset ι)
(f : ι → M)
{a : ι}
(h : a ∈ s)
:
A variant of Finset.mul_prod_erase with the multiplication swapped.
theorem
Finset.sum_erase_add
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq ι]
(s : Finset ι)
(f : ι → M)
{a : ι}
(h : a ∈ s)
:
A variant of Finset.add_sum_erase with the addition swapped.
theorem
Finset.prod_erase
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
[DecidableEq ι]
(s : Finset ι)
{f : ι → M}
{a : ι}
(h : f a = 1)
:
If a function applied at a point is 1, a product is unchanged by
removing that point, if present, from a Finset.
theorem
Finset.sum_erase
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq ι]
(s : Finset ι)
{f : ι → M}
{a : ι}
(h : f a = 0)
:
If a function applied at a point is 0, a sum is unchanged by
removing that point, if present, from a Finset.
theorem
Finset.prod_erase_lt_of_one_lt
{ι : Type u_1}
{κ : Type u_5}
[DecidableEq ι]
[CommMonoid κ]
[LT κ]
[MulLeftStrictMono κ]
{s : Finset ι}
{d : ι}
(hd : d ∈ s)
{f : ι → κ}
(hdf : 1 < f d)
:
theorem
Finset.sum_erase_lt_of_pos
{ι : Type u_1}
{κ : Type u_5}
[DecidableEq ι]
[AddCommMonoid κ]
[LT κ]
[AddLeftStrictMono κ]
{s : Finset ι}
{d : ι}
(hd : d ∈ s)
{f : ι → κ}
(hdf : 0 < f d)
:
theorem
Finset.eq_one_of_prod_eq_one
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
{s : Finset ι}
{f : ι → M}
{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_1}
{M : Type u_4}
[AddCommMonoid M]
{s : Finset ι}
{f : ι → M}
{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_biUnion_of_pairwise_eq_one
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
{f : ι → M}
[DecidableEq ι]
{s : Finset κ}
{t : κ → Finset ι}
(hs : (↑s).Pairwise fun (i j : κ) => ∀ k ∈ t i ∩ t j, f k = 1)
:
theorem
Finset.sum_biUnion_of_pairwise_eq_zero
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
{f : ι → M}
[DecidableEq ι]
{s : Finset κ}
{t : κ → Finset ι}
(hs : (↑s).Pairwise fun (i j : κ) => ∀ k ∈ t i ∩ t j, f k = 0)
:
theorem
Finset.prod_filter_of_pairwise_eq_one
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
[DecidableEq ι]
{f : κ → ι}
{g : ι → M}
{n : κ}
{I : Finset κ}
(hn : n ∈ I)
(hf : (↑I).Pairwise fun (i j : κ) => f i = f j → g (f i) = 1)
:
theorem
Finset.sum_filter_of_pairwise_eq_zero
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq ι]
{f : κ → ι}
{g : ι → M}
{n : κ}
{I : Finset κ}
(hn : n ∈ I)
(hf : (↑I).Pairwise fun (i j : κ) => f i = f j → g (f i) = 0)
:
@[simp]
theorem
Finset.prod_image_of_pairwise_eq_one
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
[DecidableEq ι]
{f : κ → ι}
{g : ι → M}
{I : Finset κ}
(hf : (↑I).Pairwise fun (i j : κ) => f i = f j → g (f i) = 1)
:
A version of Finset.prod_map and Finset.prod_image, but we do not assume that f is
injective. Rather, we assume that the image of f on I only overlaps where g (f i) = 1.
The conclusion is the same as in prod_image.
@[simp]
theorem
Finset.sum_image_of_pairwise_eq_zero
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq ι]
{f : κ → ι}
{g : ι → M}
{I : Finset κ}
(hf : (↑I).Pairwise fun (i j : κ) => f i = f j → g (f i) = 0)
:
A version of Finset.sum_map and Finset.sum_image, but we do not assume that f is
injective. Rather, we assume that the image of f on I only overlaps where g (f i) = 0.
The conclusion is the same as in sum_image.
@[simp]
theorem
Finset.prod_image_of_disjoint
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[CommMonoid M]
[DecidableEq ι]
[PartialOrder ι]
[OrderBot ι]
{f : κ → ι}
{g : ι → M}
(hg_bot : g ⊥ = 1)
{I : Finset κ}
(hf_disj : (↑I).PairwiseDisjoint f)
:
A version of Finset.prod_map and Finset.prod_image, but we do not assume that f is
injective. Rather, we assume that the images of f are disjoint on I, and g ⊥ = 1. The
conclusion is the same as in prod_image.
@[simp]
theorem
Finset.sum_image_of_disjoint
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
[AddCommMonoid M]
[DecidableEq ι]
[PartialOrder ι]
[OrderBot ι]
{f : κ → ι}
{g : ι → M}
(hg_bot : g ⊥ = 0)
{I : Finset κ}
(hf_disj : (↑I).PairwiseDisjoint f)
:
A version of Finset.sum_map and Finset.sum_image, but we do not assume that f is
injective. Rather, we assume that the images of f are disjoint on I, and g ⊥ = 0. The
conclusion is the same as in sum_image.
theorem
Finset.prod_unique_nonempty
{ι : Type u_1}
{M : Type u_4}
[CommMonoid M]
[Unique ι]
(s : Finset ι)
(f : ι → M)
(h : s.Nonempty)
:
theorem
Finset.sum_unique_nonempty
{ι : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
[Unique ι]
(s : Finset ι)
(f : ι → M)
(h : s.Nonempty)
:
theorem
Finset.prod_dvd_prod_of_dvd
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
(f g : ι → M)
(h : ∀ i ∈ s, f i ∣ g i)
:
theorem
Finset.prod_map_equiv
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
{f : ι → M}
(e : ι ≃ κ)
:
theorem
Finset.sum_map_equiv
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
{f : ι → M}
(e : ι ≃ κ)
:
theorem
Finset.prod_comp_equiv
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
{s : Finset ι}
[CommMonoid M]
{f : κ → M}
(e : ι ≃ κ)
:
theorem
Finset.sum_comp_equiv
{ι : Type u_1}
{κ : Type u_2}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
{f : κ → M}
(e : ι ≃ κ)
:
theorem
Finset.prod_sdiff_eq_prod_sdiff_iff
{ι : Type u_1}
{M : Type u_4}
[DecidableEq ι]
[CancelCommMonoid M]
{s t : Finset ι}
{f : ι → M}
:
theorem
Finset.sum_sdiff_eq_sum_sdiff_iff
{ι : Type u_1}
{M : Type u_4}
[DecidableEq ι]
[AddCancelCommMonoid M]
{s t : Finset ι}
{f : ι → M}
:
theorem
Finset.prod_sdiff_ne_prod_sdiff_iff
{ι : Type u_1}
{M : Type u_4}
[DecidableEq ι]
[CancelCommMonoid M]
{s t : Finset ι}
{f : ι → M}
:
theorem
Finset.sum_sdiff_ne_sum_sdiff_iff
{ι : Type u_1}
{M : Type u_4}
[DecidableEq ι]
[AddCancelCommMonoid M]
{s t : Finset ι}
{f : ι → M}
:
theorem
Finset.prod_insert_div
{ι : Type u_1}
{G : Type u_3}
{s : Finset ι}
{a : ι}
[CommGroup G]
[DecidableEq ι]
(ha : a ∉ s)
(f : ι → G)
:
theorem
Finset.sum_insert_sub
{ι : Type u_1}
{G : Type u_3}
{s : Finset ι}
{a : ι}
[AddCommGroup G]
[DecidableEq ι]
(ha : a ∉ s)
(f : ι → G)
:
@[simp]
theorem
Finset.sum_erase_eq_sub
{ι : Type u_1}
{G : Type u_3}
{s : Finset ι}
[AddCommGroup G]
[DecidableEq ι]
{f : ι → G}
{a : ι}
(h : a ∈ s)
:
@[simp]
theorem
Finset.sum_sdiff_eq_sub
{ι : Type u_1}
{G : Type u_3}
{s₁ s₂ : Finset ι}
[AddCommGroup G]
[DecidableEq ι]
{f : ι → G}
(h : s₁ ⊆ s₂)
:
theorem
Finset.sum_sdiff_sub_sum_sdiff
{ι : Type u_1}
{G : Type u_3}
{s₁ s₂ : Finset ι}
[AddCommGroup G]
[DecidableEq ι]
{f : ι → G}
:
theorem
Finset.sum_range_tsub
{M : Type u_4}
[AddCommMonoid M]
[PartialOrder M]
[Sub M]
[OrderedSub M]
[AddLeftMono M]
[AddLeftReflectLE M]
[ExistsAddOfLE M]
{f : ℕ → M}
(h : Monotone f)
(n : ℕ)
:
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}
{M : Type u_4}
[AddCommMonoid M]
[PartialOrder M]
[Sub M]
[OrderedSub M]
[AddLeftMono M]
[AddLeftReflectLE M]
[ExistsAddOfLE M]
(s : Finset ι)
{f g : ι → M}
(hfg : ∀ x ∈ s, g x ≤ f x)
:
@[simp]
theorem
Finset.card_disjiUnion
{ι : Type u_1}
{M : Type u_4}
(s : Finset ι)
(t : ι → Finset M)
(h : (↑s).PairwiseDisjoint t)
:
theorem
Finset.card_biUnion
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[DecidableEq M]
{t : ι → Finset M}
(h : (↑s).PairwiseDisjoint t)
:
theorem
Finset.card_eq_sum_card_fiberwise
{ι : Type u_1}
{M : Type u_4}
[DecidableEq M]
{f : ι → M}
{s : Finset ι}
{t : Finset M}
(H : Set.MapsTo f ↑s ↑t)
:
theorem
Fintype.prod_of_injective
{M : Type u_4}
{κ : Type u_6}
{ι : Type u_7}
[Fintype ι]
[Fintype κ]
[CommMonoid M]
(e : ι → κ)
(he : Function.Injective e)
(f : ι → M)
(g : κ → M)
(h' : ∀ i ∉ Set.range e, g i = 1)
(h : ∀ (i : ι), f i = g (e i))
:
theorem
Fintype.sum_of_injective
{M : Type u_4}
{κ : Type u_6}
{ι : Type u_7}
[Fintype ι]
[Fintype κ]
[AddCommMonoid M]
(e : ι → κ)
(he : Function.Injective e)
(f : ι → M)
(g : κ → M)
(h' : ∀ i ∉ Set.range e, g i = 0)
(h : ∀ (i : ι), f i = g (e i))
:
theorem
Fintype.prod_fiberwise
{M : Type u_4}
{κ : Type u_6}
{ι : Type u_7}
[Fintype ι]
[Fintype κ]
[CommMonoid M]
[DecidableEq κ]
(g : ι → κ)
(f : ι → M)
:
theorem
Fintype.sum_fiberwise
{M : Type u_4}
{κ : Type u_6}
{ι : Type u_7}
[Fintype ι]
[Fintype κ]
[AddCommMonoid M]
[DecidableEq κ]
(g : ι → κ)
(f : ι → M)
:
theorem
Fintype.prod_fiberwise'
{M : Type u_4}
{κ : Type u_6}
{ι : Type u_7}
[Fintype ι]
[Fintype κ]
[CommMonoid M]
[DecidableEq κ]
(g : ι → κ)
(f : κ → M)
:
theorem
Fintype.sum_fiberwise'
{M : Type u_4}
{κ : Type u_6}
{ι : Type u_7}
[Fintype ι]
[Fintype κ]
[AddCommMonoid M]
[DecidableEq κ]
(g : ι → κ)
(f : κ → M)
:
theorem
Fintype.prod_unique
{M : Type u_4}
{ι : Type u_7}
[Fintype ι]
[CommMonoid M]
[Unique ι]
(f : ι → M)
:
theorem
Fintype.sum_unique
{M : Type u_4}
{ι : Type u_7}
[Fintype ι]
[AddCommMonoid M]
[Unique ι]
(f : ι → M)
:
theorem
Fintype.prod_subsingleton
{M : Type u_4}
{ι : Type u_7}
[Fintype ι]
[CommMonoid M]
[Subsingleton ι]
(f : ι → M)
(a : ι)
:
theorem
Fintype.sum_subsingleton
{M : Type u_4}
{ι : Type u_7}
[Fintype ι]
[AddCommMonoid M]
[Subsingleton ι]
(f : ι → M)
(a : ι)
:
theorem
Fintype.prod_subset
{M : Type u_4}
{ι : Type u_7}
[Fintype ι]
[CommMonoid M]
{s : Finset ι}
{f : ι → M}
(h : ∀ (i : ι), f i ≠ 1 → i ∈ s)
:
theorem
Fintype.sum_subset
{M : Type u_4}
{ι : Type u_7}
[Fintype ι]
[AddCommMonoid M]
{s : Finset ι}
{f : ι → M}
(h : ∀ (i : ι), f i ≠ 0 → i ∈ s)
:
theorem
List.prod_toFinset
{ι : Type u_1}
{M : Type u_5}
[DecidableEq ι]
[CommMonoid M]
(f : ι → M)
{l : List ι}
(_hl : l.Nodup)
:
theorem
List.sum_toFinset
{ι : Type u_1}
{M : Type u_5}
[DecidableEq ι]
[AddCommMonoid M]
(f : ι → M)
{l : List ι}
(_hl : l.Nodup)
:
@[simp]
@[simp]
theorem
Multiset.sum_count_eq_card
{ι : Type u_1}
[DecidableEq ι]
{s : Finset ι}
{m : Multiset ι}
(hms : ∀ a ∈ m, a ∈ s)
:
theorem
Multiset.prod_sum
{M : Type u_4}
{ι : Type u_5}
[CommMonoid M]
(f : ι → Multiset M)
(s : Finset ι)
:
theorem
Multiset.sum_sum
{M : Type u_4}
{ι : Type u_5}
[AddCommMonoid M]
(f : ι → Multiset M)
(s : Finset ι)
:
@[simp]
@[simp]
theorem
IsAddUnit.sum_iff
{ι : Type u_1}
{M : Type u_4}
{s : Finset ι}
[AddCommMonoid M]
{f : ι → M}
:
theorem
IsAddUnit.sum_univ_iff
{ι : Type u_1}
{M : Type u_4}
[Fintype ι]
[AddCommMonoid M]
{f : ι → M}
:
@[deprecated Int.natAbs_sum_le (since := "2026-02-14")]
Alias of Int.natAbs_sum_le.