theorem
Finset.prod_eq_fold
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(s : Finset α)
(f : α → β)
:
theorem
Finset.sum_eq_fold
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset α)
(f : α → β)
:
theorem
MonoidHom.coe_finset_prod
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[MulOneClass β]
[CommMonoid γ]
(f : α → β →* γ)
(s : Finset α)
:
theorem
AddMonoidHom.coe_finset_sum
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddZeroClass β]
[AddCommMonoid γ]
(f : α → β →+ γ)
(s : Finset α)
:
@[simp]
theorem
MonoidHom.finset_prod_apply
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[MulOneClass β]
[CommMonoid γ]
(f : α → β →* γ)
(s : Finset α)
(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 : β)
:
See also Finset.sum_apply, with the same conclusion but with the weaker hypothesis
f : α → β → γ
@[simp]
theorem
Finset.prod_cons
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{a : α}
{f : α → β}
[CommMonoid β]
(h : a ∉ s)
:
@[simp]
theorem
Finset.sum_cons
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{a : α}
{f : α → β}
[AddCommMonoid β]
(h : a ∉ s)
:
@[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]
@[simp]
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_image
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
{s : Finset γ}
{g : γ → α}
:
@[simp]
theorem
Finset.sum_image
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset γ}
{g : γ → α}
:
theorem
Finset.prod_attach
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(s : Finset α)
(f : α → β)
:
theorem
Finset.sum_attach
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset α)
(f : α → β)
:
theorem
Finset.prod_eq_one
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
{f : α → β}
{s : Finset α}
(h : ∀ 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)
:
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)
:
theorem
Finset.sum_disjiUnion
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[AddCommMonoid β]
(s : Finset ι)
(t : ι → Finset α)
(h : (↑s).PairwiseDisjoint t)
:
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 : α → β)
:
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 : α → β)
:
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 : α → β)
:
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 : α → β)
:
theorem
Finset.prod_filter_xor
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommMonoid β]
(p q : α → Prop)
[DecidablePred p]
[DecidablePred q]
:
theorem
Finset.sum_filter_xor
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
(p q : α → Prop)
[DecidablePred p]
[DecidablePred q]
:
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)
:
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)
:
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)
:
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)
:
@[deprecated Finset.prod_sumElim (since := "2025-02-20")]
theorem
Finset.prod_sum_elim
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[CommMonoid β]
(s : Finset α)
(t : Finset γ)
(f : α → β)
(g : γ → β)
:
Alias of Finset.prod_sumElim.
@[deprecated Finset.sum_sumElim (since := "2025-02-20")]
theorem
Finset.sum_sum_elim
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[AddCommMonoid β]
(s : Finset α)
(t : Finset γ)
(f : α → β)
(g : γ → β)
:
Alias of Finset.sum_sumElim.
theorem
Finset.prod_biUnion
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{f : α → β}
[CommMonoid β]
[DecidableEq α]
{s : Finset γ}
{t : γ → Finset α}
(hs : (↑s).PairwiseDisjoint t)
:
theorem
Finset.sum_biUnion
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
{f : α → β}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset γ}
{t : γ → Finset α}
(hs : (↑s).PairwiseDisjoint t)
:
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))
:
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))
:
theorem
Finset.prod_fiberwise_eq_prod_filter
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
[DecidableEq κ]
(s : Finset ι)
(t : Finset κ)
(g : ι → κ)
(f : ι → α)
:
theorem
Finset.sum_fiberwise_eq_sum_filter
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
[DecidableEq κ]
(s : Finset ι)
(t : Finset κ)
(g : ι → κ)
(f : ι → α)
:
theorem
Finset.prod_fiberwise_eq_prod_filter'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
[DecidableEq κ]
(s : Finset ι)
(t : Finset κ)
(g : ι → κ)
(f : κ → α)
:
theorem
Finset.sum_fiberwise_eq_sum_filter'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
[DecidableEq κ]
(s : Finset ι)
(t : Finset κ)
(g : ι → κ)
(f : κ → α)
:
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 : ι → α)
:
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 : ι → α)
:
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 : κ → α)
:
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 : κ → α)
:
theorem
Finset.prod_fiberwise
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
[DecidableEq κ]
[Fintype κ]
(s : Finset ι)
(g : ι → κ)
(f : ι → α)
:
theorem
Finset.sum_fiberwise
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
[DecidableEq κ]
[Fintype κ]
(s : Finset ι)
(g : ι → κ)
(f : ι → α)
:
theorem
Finset.prod_fiberwise'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[CommMonoid α]
[DecidableEq κ]
[Fintype κ]
(s : Finset ι)
(g : ι → κ)
(f : κ → α)
:
theorem
Finset.sum_fiberwise'
{ι : Type u_6}
{κ : Type u_7}
{α : Type u_8}
[AddCommMonoid α]
[DecidableEq κ]
[Fintype κ]
(s : Finset ι)
(g : ι → κ)
(f : κ → α)
:
@[simp]
theorem
Finset.prod_diag
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α × α → β)
:
@[simp]
theorem
Finset.sum_diag
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
(s : Finset α)
(f : α × α → β)
:
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 ∈ {j ∈ s | g j = g i}, h j)
:
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 ∈ {j ∈ s | g j = g i}, h j)
:
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_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)
:
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)
:
theorem
Finset.prod_filter_ne_one
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[CommMonoid β]
(s : Finset α)
[(x : α) → Decidable (f x ≠ 1)]
:
theorem
Finset.sum_filter_ne_zero
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[AddCommMonoid β]
(s : Finset α)
[(x : α) → Decidable (f x ≠ 0)]
:
theorem
Finset.prod_filter
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[CommMonoid β]
(p : α → Prop)
[DecidablePred p]
(f : α → β)
:
theorem
Finset.sum_filter
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[AddCommMonoid β]
(p : α → Prop)
[DecidablePred p]
(f : α → β)
:
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)
:
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)
:
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)
:
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)
:
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]
:
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]
:
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)
:
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)
:
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)
:
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)
:
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_finset_coe
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
(f : α → β)
(s : Finset α)
:
theorem
Finset.sum_finset_coe
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(f : α → β)
(s : Finset α)
:
theorem
Finset.prod_set_coe
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[CommMonoid β]
(s : Set α)
[Fintype ↑s]
:
theorem
Finset.sum_set_coe
{α : Type u_3}
{β : Type u_4}
{f : α → β}
[AddCommMonoid β]
(s : Set α)
[Fintype ↑s]
:
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)
:
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)
:
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 : γ → β)
:
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 : γ → β)
:
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 : γ → β)
:
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 : γ → β)
:
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 → β)
:
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 → β)
:
theorem
Finset.prod_ite
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
{s : Finset α}
{p : α → Prop}
{hp : DecidablePred p}
(f g : α → β)
:
theorem
Finset.sum_ite
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
{s : Finset α}
{p : α → Prop}
{hp : DecidablePred p}
(f g : α → β)
:
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 : α → β)
:
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 : α → β)
:
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 : α → β)
:
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 : α → β)
:
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)
:
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)
:
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)
:
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)
:
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 : α → β)
:
theorem
Finset.prod_eq_prod_extend
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[CommMonoid β]
(f : { x : α // x ∈ s } → β)
:
theorem
Finset.sum_eq_sum_extend
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[AddCommMonoid β]
(f : { x : α // x ∈ s } → β)
:
@[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 : α → β)
:
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)
:
@[simp]
theorem
Finset.prod_pi_mulSingle'
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
(a : α)
(x : β)
(s : Finset α)
:
@[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 α)
:
@[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 : ι → α → β)
:
theorem
Finset.support_sum
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
(s : Finset ι)
(f : ι → α → β)
:
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)
:
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)
:
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)
:
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)
:
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]
:
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]
:
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 : ι → κ → β)
:
theorem
Finset.mulIndicator_biUnion
{ι : Type u_1}
{β : Type u_4}
[CommMonoid β]
{κ : Type u_7}
(s : Finset ι)
(t : ι → Set κ)
{f : κ → β}
(hs : (↑s).PairwiseDisjoint t)
:
theorem
Finset.indicator_biUnion
{ι : Type u_1}
{β : Type u_4}
[AddCommMonoid β]
{κ : Type u_7}
(s : Finset ι)
(t : ι → Set κ)
{f : κ → β}
(hs : (↑s).PairwiseDisjoint t)
:
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 : κ)
:
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 : κ)
:
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₂))
:
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₂))
:
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_list_map_count
{α : Type u_3}
[DecidableEq α]
(l : List α)
{M : Type u_6}
[CommMonoid M]
(f : α → M)
:
theorem
Finset.sum_list_map_count
{α : Type u_3}
[DecidableEq α]
(l : List α)
{M : Type u_6}
[AddCommMonoid M]
(f : α → M)
:
theorem
Finset.prod_list_count_of_subset
{α : Type u_3}
[DecidableEq α]
[CommMonoid α]
(m : List α)
(s : Finset α)
(hs : m.toFinset ⊆ s)
:
theorem
Finset.sum_list_count_of_subset
{α : Type u_3}
[DecidableEq α]
[AddCommMonoid α]
(m : List α)
(s : Finset α)
(hs : m.toFinset ⊆ s)
:
theorem
Finset.prod_multiset_map_count
{α : Type u_3}
[DecidableEq α]
(s : Multiset α)
{M : Type u_6}
[CommMonoid M]
(f : α → M)
:
theorem
Finset.sum_multiset_map_count
{α : Type u_3}
[DecidableEq α]
(s : Multiset α)
{M : Type u_6}
[AddCommMonoid M]
(f : α → M)
:
theorem
Finset.sum_multiset_count
{α : Type u_3}
[DecidableEq α]
[AddCommMonoid α]
(s : Multiset α)
:
theorem
Finset.prod_multiset_count_of_subset
{α : Type u_3}
[DecidableEq α]
[CommMonoid α]
(m : Multiset α)
(s : Finset α)
(hs : m.toFinset ⊆ s)
:
theorem
Finset.sum_multiset_count_of_subset
{α : Type u_3}
[DecidableEq α]
[AddCommMonoid α]
(m : Multiset α)
(s : Finset α)
(hs : m.toFinset ⊆ s)
:
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 : ℕ)
:
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 : ℕ)
:
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_tsub
{α : Type u_3}
[AddCommMonoid α]
[PartialOrder α]
[Sub α]
[OrderedSub α]
[AddLeftMono α]
[AddLeftReflectLE α]
[ExistsAddOfLE α]
{f : ℕ → α}
(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}
{α : 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.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_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)
:
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)
:
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)
:
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)
:
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 : α → γ)
:
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 : α → γ)
:
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)
:
theorem
Finset.prod_partition
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommMonoid β]
(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_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
(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_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[CommMonoid β]
(R : Setoid α)
[DecidableRel ⇑R]
(h : ∀ x ∈ s, ∏ a ∈ {a ∈ s | 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_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommMonoid β]
(R : Setoid α)
[DecidableRel ⇑R]
(h : ∀ x ∈ s, ∑ a ∈ {a ∈ s | R a x}, f a = 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 : β)
:
theorem
Finset.sum_update_of_not_mem
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∉ s)
(f : α → β)
(b : β)
:
theorem
Finset.prod_update_of_mem
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
(b : β)
:
theorem
Finset.sum_update_of_mem
{α : Type u_3}
{β : Type u_4}
[AddCommMonoid β]
[DecidableEq α]
{s : Finset α}
{i : α}
(h : i ∈ s)
(f : α → β)
(b : β)
:
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)
:
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)
:
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_3}
{γ : Type u_6}
[DecidableEq α]
[CommMonoid γ]
[LT γ]
[MulLeftStrictMono γ]
{s : Finset α}
{d : α}
(hd : d ∈ s)
{f : α → γ}
(hdf : 1 < f d)
:
theorem
Finset.sum_erase_lt_of_pos
{α : Type u_3}
{γ : Type u_6}
[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_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_dvd_prod_of_dvd
{α : Type u_3}
{β : Type u_4}
[CommMonoid β]
{S : Finset α}
(g1 g2 : α → β)
(h : ∀ a ∈ S, g1 a ∣ g2 a)
:
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 : ι → α}
:
@[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.sum_erase_eq_sub
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
{f : α → β}
[AddCommGroup β]
[DecidableEq α]
{a : α}
(h : a ∈ s)
:
@[simp]
theorem
Finset.card_disjiUnion
{α : Type u_3}
{β : Type u_4}
(s : Finset α)
(t : α → Finset β)
(h : (↑s).PairwiseDisjoint t)
:
theorem
Finset.card_biUnion
{α : Type u_3}
{β : Type u_4}
{s : Finset α}
[DecidableEq β]
{t : α → Finset β}
(h : (↑s).PairwiseDisjoint t)
:
theorem
Finset.card_eq_sum_card_fiberwise
{α : Type u_3}
{β : Type u_4}
[DecidableEq β]
{f : α → β}
{s : Finset α}
{t : Finset β}
(H : Set.MapsTo f ↑s ↑t)
:
theorem
Finset.prod_unique_nonempty
{α : Type u_6}
{β : Type u_7}
[CommMonoid β]
[Unique α]
(s : Finset α)
(f : α → β)
(h : s.Nonempty)
:
theorem
Finset.sum_unique_nonempty
{α : Type u_6}
{β : Type u_7}
[AddCommMonoid β]
[Unique α]
(s : Finset α)
(f : α → β)
(h : s.Nonempty)
:
theorem
Finset.prod_filter_of_pairwise_eq_one
{α : Type u_6}
{β : Type u_7}
{ι : Type u_8}
[DecidableEq α]
[CommMonoid β]
{f : ι → α}
{g : α → β}
{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_6}
{β : Type u_7}
{ι : Type u_8}
[DecidableEq α]
[AddCommMonoid β]
{f : ι → α}
{g : α → β}
{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_6}
{β : Type u_7}
{ι : Type u_8}
[DecidableEq α]
[CommMonoid β]
{f : ι → α}
{g : α → β}
{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_6}
{β : Type u_7}
{ι : Type u_8}
[DecidableEq α]
[AddCommMonoid β]
{f : ι → α}
{g : α → β}
{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_6}
{β : Type u_7}
{ι : Type u_8}
[DecidableEq α]
[CommMonoid β]
[PartialOrder α]
[OrderBot α]
{f : ι → α}
{g : α → β}
(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_6}
{β : Type u_7}
{ι : Type u_8}
[DecidableEq α]
[AddCommMonoid β]
[PartialOrder α]
[OrderBot α]
{f : ι → α}
{g : α → β}
(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
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))
:
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))
:
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 : α → β)
:
theorem
Fintype.sum_unique
{α : Type u_9}
{β : Type u_10}
[AddCommMonoid β]
[Unique α]
[Fintype α]
(f : α → β)
:
theorem
Fintype.prod_subsingleton
{α : Type u_9}
{β : Type u_10}
[CommMonoid β]
[Subsingleton α]
[Fintype α]
(f : α → β)
(a : α)
:
theorem
Fintype.sum_subsingleton
{α : Type u_9}
{β : Type u_10}
[AddCommMonoid β]
[Subsingleton α]
[Fintype α]
(f : α → β)
(a : α)
:
theorem
Fintype.prod_subset
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[CommMonoid α]
{s : Finset ι}
{f : ι → α}
(h : ∀ (i : ι), f i ≠ 1 → i ∈ s)
:
theorem
Fintype.sum_subset
{ι : Type u_6}
{α : Type u_8}
[Fintype ι]
[AddCommMonoid α]
{s : Finset ι}
{f : ι → α}
(h : ∀ (i : ι), f i ≠ 0 → i ∈ s)
:
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)
:
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 : α)
:
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'.
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]
@[simp]
theorem
Multiset.sum_count_eq_card
{α : Type u_3}
[DecidableEq α]
{s : Finset α}
{m : Multiset α}
(hms : ∀ a ∈ m, a ∈ s)
:
theorem
Multiset.prod_sum
{α : Type u_6}
{ι : Type u_7}
[CommMonoid α]
(f : ι → Multiset α)
(s : Finset ι)
:
theorem
Multiset.sum_sum
{α : Type u_6}
{ι : Type u_7}
[AddCommMonoid α]
(f : ι → Multiset α)
(s : Finset ι)
:
@[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 β]
: