card_derangements_invariant — Mathlib

English

If α and β are finite with the same cardinality, then the number of derangements of α equals the number of derangements of β.

Русский

Если множества α и β конечно и имеют одинаковую мощность, то число перестановок без фиксаций точек на α равно числу таких перестановок на β.

LaTeX

$$$|\\mathrm{derangements}(\\alpha)| = |\\mathrm{derangements}(\\beta)|$ given $|\\alpha| = |\\beta|$ and finiteness/decidability assumptions$$

Lean4

theorem card_derangements_invariant {α β : Type*} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β]
    (h : card α = card β) : card (derangements α) = card (derangements β) :=
  Fintype.card_congr (Equiv.derangementsCongr <| equivOfCardEq h)

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