card_perm — Mathlib

English

If α is finite, the number of bijections from α to itself (the permutation group) equals the factorial of the size of α.

Русский

Если множество α конечно, то число биекций α → α (группа перестановок) равно факториалу размера α.

LaTeX

$$$ |\\operatorname{Perm}(\\alpha)| = |\\alpha|! $$$

Lean4

theorem card_perm {α : Type*} [Finite α] : Nat.card (Equiv.Perm α) = (Nat.card α)! := by
  classical
  have := Fintype.ofFinite α
  rw [card_eq_fintype_card, card_eq_fintype_card, Fintype.card_perm]

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