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.Basic
and should be moved at some point.
theorem
Fintype.card_eq_sum_ones
{α : Type u_4}
[Fintype α]
:
Fintype.card α = Finset.univ.sum fun (_a : α) => 1
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)
:
(Finset.univ.sum fun (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)
:
(Finset.univ.prod fun (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)
:
(Finset.univ.sum fun (a : α) => f a) = Finset.univ.sum fun (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)
:
(Finset.univ.prod fun (a : α) => f a) = Finset.univ.prod fun (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)
:
(Finset.univ.sum fun (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)
:
(Finset.univ.prod fun (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 : (s.sum fun (i : ι) => 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 : (s.prod fun (i : ι) => 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 = s.prod fun (i : ι) => (t i).card
@[simp]
theorem
Fintype.card_piFinset
{ι : Type u_4}
{α : ι → Type u_6}
[DecidableEq ι]
[Fintype ι]
(s : (i : ι) → Finset (α i))
:
(Fintype.piFinset s).card = Finset.univ.prod fun (i : ι) => (s i).card
@[simp]
theorem
Fintype.card_pi
{ι : Type u_4}
{α : ι → Type u_6}
[Fintype ι]
[DecidableEq ι]
[(i : ι) → Fintype (α i)]
:
Fintype.card ((i : ι) → α i) = Finset.univ.prod fun (i : ι) => Fintype.card (α i)
@[simp]
theorem
Fintype.card_sigma
{ι : Type u_4}
{α : ι → Type u_6}
[Fintype ι]
[(i : ι) → Fintype (α i)]
:
Fintype.card (Sigma α) = Finset.univ.sum fun (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 = (Finset.univ.erase i).prod fun (j : ι) => (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 (Finset.univ.erase i).prod fun (b : ι) => (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 : ℕ)
:
(Finset.univ.sum fun (i : Fin n) => f ↑i) = (Finset.range n).sum fun (i : ℕ) => 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 : ℕ)
:
(Finset.univ.prod fun (i : Fin n) => f ↑i) = (Finset.range n).prod fun (i : ℕ) => 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 → β)
:
(Finset.univ.sum fun (i : Fin n) => c i) = (Finset.range n).sum fun (i : ℕ) => 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 → β)
:
(Finset.univ.prod fun (i : Fin n) => c i) = (Finset.range n).prod fun (i : ℕ) => 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.