Results about "big operations" over a Fintype, and consequent
results about cardinalities of certain types.
Implementation note #
This content had previously been in Data.Fintype.Basic, but was moved here to avoid
requiring Algebra.BigOperators (and hence many other imports) as a
dependency of Fintype.
However many of the results here really belong in Algebra.BigOperators.Group.Finset
and should be moved at some point.
theorem
Fintype.sum_extend_by_zero
{α : Type u_1}
{ι : Type u_4}
[DecidableEq ι]
[Fintype ι]
[AddCommMonoid α]
(s : Finset ι)
(f : ι → α)
:
theorem
Fintype.prod_extend_by_one
{α : Type u_1}
{ι : Type u_4}
[DecidableEq ι]
[Fintype ι]
[CommMonoid α]
(s : Finset ι)
(f : ι → α)
:
theorem
Fintype.sum_eq_zero
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[AddCommMonoid M]
(f : α → M)
(h : ∀ (a : α), f a = 0)
:
∑ a : α, f a = 0
theorem
Fintype.prod_eq_one
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[CommMonoid M]
(f : α → M)
(h : ∀ (a : α), f a = 1)
:
∏ a : α, f a = 1
theorem
Fintype.sum_congr
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[AddCommMonoid M]
(f : α → M)
(g : α → M)
(h : ∀ (a : α), f a = g a)
:
∑ a : α, f a = ∑ a : α, g a
theorem
Fintype.prod_congr
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[CommMonoid M]
(f : α → M)
(g : α → M)
(h : ∀ (a : α), f a = g a)
:
∏ a : α, f a = ∏ a : α, g a
theorem
Fintype.sum_eq_single
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[AddCommMonoid M]
{f : α → M}
(a : α)
(h : ∀ (x : α), x ≠ a → f x = 0)
:
∑ x : α, f x = f a
theorem
Fintype.prod_eq_single
{α : Type u_1}
{M : Type u_4}
[Fintype α]
[CommMonoid M]
{f : α → M}
(a : α)
(h : ∀ (x : α), x ≠ a → f x = 1)
:
∏ x : α, f x = f a
theorem
Fintype.eq_of_subsingleton_of_sum_eq
{M : Type u_4}
[AddCommMonoid M]
{ι : Type u_5}
[Subsingleton ι]
{s : Finset ι}
{f : ι → M}
{b : M}
(h : ∑ i ∈ s, f i = b)
(i : ι)
:
If a sum of a Finset of a subsingleton type has a given
value, so do the terms in that sum.
theorem
Fintype.eq_of_subsingleton_of_prod_eq
{M : Type u_4}
[CommMonoid M]
{ι : Type u_5}
[Subsingleton ι]
{s : Finset ι}
{f : ι → M}
{b : M}
(h : ∏ i ∈ s, f i = b)
(i : ι)
:
If a product of a Finset of a subsingleton type has a given
value, so do the terms in that product.
@[simp]
theorem
Finset.card_pi
{ι : Type u_4}
{α : ι → Type u_6}
[DecidableEq ι]
(s : Finset ι)
(t : (i : ι) → Finset (α i))
:
(s.pi t).card = ∏ i ∈ s, (t i).card
@[simp]
theorem
Fintype.card_piFinset
{ι : Type u_4}
{α : ι → Type u_6}
[DecidableEq ι]
[Fintype ι]
(s : (i : ι) → Finset (α i))
:
(Fintype.piFinset s).card = ∏ i : ι, (s i).card
@[simp]
theorem
Fintype.card_pi
{ι : Type u_4}
{α : ι → Type u_6}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → Fintype (α i)]
:
Fintype.card ((i : ι) → α i) = ∏ i : ι, Fintype.card (α i)
@[simp]
theorem
Fintype.card_sigma
{ι : Type u_4}
{α : ι → Type u_6}
[Fintype ι]
[(i : ι) → Fintype (α i)]
:
Fintype.card (Sigma α) = ∑ i : ι, Fintype.card (α i)
theorem
Fintype.card_filter_piFinset_eq_of_mem
{ι : Type u_4}
{α : ι → Type u_6}
[DecidableEq ι]
[Fintype ι]
[(i : ι) → DecidableEq (α i)]
(s : (i : ι) → Finset (α i))
(i : ι)
{a : α i}
(ha : a ∈ s i)
:
(Finset.filter (fun (f : (a : ι) → α a) => f i = a) (Fintype.piFinset s)).card = ∏ j ∈ Finset.univ.erase i, (s j).card
The number of dependent maps f : Π j, s j for which the i component is a is the product
over all j ≠ i of (s j).card.
Note that this is just a composition of easier lemmas, but there's some glue missing to make that smooth enough not to need this lemma.
theorem
Fintype.card_filter_piFinset_const_eq_of_mem
{ι : Type u_4}
{κ : Type u_5}
[DecidableEq ι]
[DecidableEq κ]
[Fintype ι]
(s : Finset κ)
(i : ι)
{x : κ}
(hx : x ∈ s)
:
(Finset.filter (fun (f : ι → κ) => f i = x) (Fintype.piFinset fun (x : ι) => s)).card = s.card ^ (Fintype.card ι - 1)
theorem
Fintype.card_filter_piFinset_eq
{ι : Type u_4}
{α : ι → Type u_6}
[DecidableEq ι]
[Fintype ι]
[(i : ι) → DecidableEq (α i)]
(s : (i : ι) → Finset (α i))
(i : ι)
(a : α i)
:
(Finset.filter (fun (f : (a : ι) → α a) => f i = a) (Fintype.piFinset s)).card = if a ∈ s i then ∏ b ∈ Finset.univ.erase i, (s b).card else 0
theorem
Fintype.card_filter_piFinset_const
{ι : Type u_4}
{κ : Type u_5}
[DecidableEq ι]
[DecidableEq κ]
[Fintype ι]
(s : Finset κ)
(i : ι)
(j : κ)
:
(Finset.filter (fun (f : ι → κ) => f i = j) (Fintype.piFinset fun (x : ι) => s)).card = if j ∈ s then s.card ^ (Fintype.card ι - 1) else 0
theorem
Fintype.card_fun
{α : Type u_1}
{β : Type u_2}
[DecidableEq α]
[Fintype α]
[Fintype β]
:
Fintype.card (α → β) = Fintype.card β ^ Fintype.card α
@[simp]
theorem
card_vector
{α : Type u_1}
[Fintype α]
(n : ℕ)
:
Fintype.card (Vector α n) = Fintype.card α ^ n
theorem
Fin.sum_univ_eq_sum_range
{α : Type u_1}
[AddCommMonoid α]
(f : ℕ → α)
(n : ℕ)
:
∑ i : Fin n, f ↑i = ∑ i ∈ Finset.range n, f i
It is equivalent to sum a function over fin n or finset.range n.
theorem
Fin.prod_univ_eq_prod_range
{α : Type u_1}
[CommMonoid α]
(f : ℕ → α)
(n : ℕ)
:
∏ i : Fin n, f ↑i = ∏ i ∈ Finset.range n, f i
It is equivalent to compute the product of a function over Fin n or Finset.range n.
theorem
Finset.sum_fin_eq_sum_range
{β : Type u_2}
[AddCommMonoid β]
{n : ℕ}
(c : Fin n → β)
:
∑ i : Fin n, c i = ∑ i ∈ Finset.range n, if h : i < n then c ⟨i, h⟩ else 0
theorem
Finset.prod_fin_eq_prod_range
{β : Type u_2}
[CommMonoid β]
{n : ℕ}
(c : Fin n → β)
:
∏ i : Fin n, c i = ∏ i ∈ Finset.range n, if h : i < n then c ⟨i, h⟩ else 1
theorem
Finset.sum_toFinset_eq_subtype
{α : Type u_1}
{M : Type u_4}
[AddCommMonoid M]
[Fintype α]
(p : α → Prop)
[DecidablePred p]
(f : α → M)
:
theorem
Finset.prod_toFinset_eq_subtype
{α : Type u_1}
{M : Type u_4}
[CommMonoid M]
[Fintype α]
(p : α → Prop)
[DecidablePred p]
(f : α → M)
:
theorem
Fintype.prod_dite
{α : Type u_1}
{β : Type u_2}
[Fintype α]
{p : α → Prop}
[DecidablePred p]
[CommMonoid β]
(f : (a : α) → p a → β)
(g : (a : α) → ¬p a → β)
:
theorem
Fintype.sum_prod_type'
{γ : Type u_3}
{α₁ : Type u_4}
{α₂ : Type u_5}
[Fintype α₁]
[Fintype α₂]
[AddCommMonoid γ]
{f : α₁ → α₂ → γ}
:
An uncurried version of Finset.sum_prod_type
theorem
Fintype.prod_prod_type'
{γ : Type u_3}
{α₁ : Type u_4}
{α₂ : Type u_5}
[Fintype α₁]
[Fintype α₂]
[CommMonoid γ]
{f : α₁ → α₂ → γ}
:
An uncurried version of Finset.prod_prod_type.
theorem
Fintype.sum_prod_type_right'
{γ : Type u_3}
{α₁ : Type u_4}
{α₂ : Type u_5}
[Fintype α₁]
[Fintype α₂]
[AddCommMonoid γ]
{f : α₁ → α₂ → γ}
:
An uncurried version of Finset.sum_prod_type_right
theorem
Fintype.prod_prod_type_right'
{γ : Type u_3}
{α₁ : Type u_4}
{α₂ : Type u_5}
[Fintype α₁]
[Fintype α₂]
[CommMonoid γ]
{f : α₁ → α₂ → γ}
:
An uncurried version of Finset.prod_prod_type_right.