card_derangements_fin_eq_numDerangements

English

For every natural n, the cardinality of the derangements on Fin(n) equals the number numDerangements(n).

Русский

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

LaTeX

$$$|\\mathrm{derangements}(\\mathrm{Fin}(n))| = \\mathrm{numDerangements}(n).$$$

Lean4

theorem card_derangements_fin_eq_numDerangements {n : ℕ} : card (derangements (Fin n)) = numDerangements n :=
  by
  induction n using Nat.strongRecOn with
  | ind n hyp => _
  rcases n with _ | _ | n
  · rfl
  ·
    rfl
      -- now we have n ≥ 2. rewrite everything in terms of card_derangements, so that we can use
        -- `card_derangements_fin_add_two`

  rw [numDerangements_add_two, card_derangements_fin_add_two, mul_add, hyp, hyp] <;> omega

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