English
The numbers D_n can be expressed as a signed sum over rising factorials: D_n = sum_{k=0}^n (-1)^k (k+1)^{overline{n-k}}.
Русский
Числа D_n выражаются как знаковая сумма по возрастающим факториалам: D_n = \\sum_{k=0}^n (-1)^k (k+1)^{\\overline{n-k}}.
LaTeX
$$$(\\mathrm{numDerangements}(n))_{\\mathbb{Z}} = \\sum_{k=0}^{n} (-1)^k \\,(k+1)^{\\overline{n-k}}.$$$
Lean4
theorem numDerangements_sum (n : ℕ) :
(numDerangements n : ℤ) = ∑ k ∈ Finset.range (n + 1), (-1 : ℤ) ^ k * Nat.ascFactorial (k + 1) (n - k) := by
induction n with
| zero => rfl
| succ n
hn =>
rw [Finset.sum_range_succ, numDerangements_succ, hn, Finset.mul_sum, tsub_self, Nat.ascFactorial_zero,
Int.ofNat_one, mul_one, pow_succ', neg_one_mul, sub_eq_add_neg, add_left_inj, Finset.sum_congr rfl]
-- show that (n + 1) * (-1)^x * asc_fac x (n - x) = (-1)^x * asc_fac x (n.succ - x)
intro x hx
have h_le : x ≤ n := Finset.mem_range_succ_iff.mp hx
rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_right_comm, add_tsub_cancel_of_le h_le, Int.natCast_mul,
Int.natCast_add, mul_left_comm, Nat.cast_one]
