Number of embeddings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 β]
[fintype (α ↪ β)] :
fintype.card (α ↪ β) = (fintype.card β).desc_factorial (fintype.card α)