card_derangements_eq_numDerangements

English

For any finite α, the cardinality of its derangements equals numDerangements(card α).

Русский

Для любого конечного множества α кардинальность перестановок без фиксаций равна numDerangements(card α).

LaTeX

$$$|\\mathrm{derangements}(\\alpha)| = \\mathrm{numDerangements}(\\#\\alpha).$$$

Lean4

theorem card_derangements_eq_numDerangements (α : Type*) [Fintype α] [DecidableEq α] :
    card (derangements α) = numDerangements (card α) :=
  by
  rw [← card_derangements_invariant (card_fin _)]
  exact card_derangements_fin_eq_numDerangements

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