numDerangements_succ — Mathlib

English

The integer form of the recurrence gives an relation between consecutive D_n’s when viewed inside the integers.

Русский

Целочисленная форма рекуррентного соотношения даёт связь между соседними D_n при просмотре внутри целых чисел.

LaTeX

$$$(\\mathrm{numDerangements}(n+1))_{\\mathbb{Z}} = (n+1)\\cdot(\\mathrm{numDerangements}(n)_{\\mathbb{Z}}) - (-1)^n.$$$

Lean4

theorem numDerangements_succ (n : ℕ) : (numDerangements (n + 1) : ℤ) = (n + 1) * (numDerangements n : ℤ) - (-1) ^ n :=
  by
  induction n with
  | zero => rfl
  | succ n hn =>
    simp only [numDerangements_add_two, hn, pow_succ, Int.natCast_mul, Int.natCast_add]
    ring

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