Number of embeddings #
This file establishes the cardinality of α ↪ β in full generality.
theorem
Fintype.card_embedding_eq_of_unique
{α : Type u_1}
{β : Type u_2}
[Unique α]
[Fintype β]
[Fintype (α ↪ β)]
:
Fintype.card (α ↪ β) = Fintype.card β
@[simp]
theorem
Fintype.card_embedding_eq
{α : Type u_1}
{β : Type u_2}
[Fintype α]
[Fintype β]
[emb : Fintype (α ↪ β)]
:
Fintype.card (α ↪ β) = Nat.descFactorial (Fintype.card β) (Fintype.card α)