card_equiv — Mathlib

English

For any equivalence e: α ≃ β between finite types, the number of equivalences α ≃ β is (card α)!.

Русский

Для любой эквивалентности e: α ≃ β между конечными типами, число эквивалентов α ≃ β равно (card α)!.

LaTeX

$$$Fintype.card(\\alpha \\simeq \\beta) = (Fintype.card \\alpha)!$$$

Lean4

theorem card_equiv [Fintype α] [Fintype β] (e : α ≃ β) : Fintype.card (α ≃ β) = (Fintype.card α)! :=
  Fintype.card_congr (equivCongr (Equiv.refl α) e) ▸ Fintype.card_perm

Похожие утверждения