Theorems · Theorem · combinatorics

Fintype.card_embedding_eq

∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] [emb : Fintype (α ↪ β)],
  Fintype.card (α ↪ β) = (Fintype.card β).descFactorial (Fintype.card α)

Defined in

Mathlib.Data.Fintype.CardEmbedding

Cited by

1 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeFintypeFintype