numDerangements — Mathlib

English

Let D_n denote the number of derangements of an n-element set. Then D_0 = 1, D_1 = 0, and D_{n+2} = (n+1)(D_n + D_{n+1}) for all n ≥ 0.

Русский

Обозначим через D_n число перестановок без фиксаций на множество из n элементов. Тогда D_0 = 1, D_1 = 0, и D_{n+2} = (n+1)(D_n + D_{n+1}) для всех n ≥ 0.

LaTeX

$$$D_0 = 1,\\; D_1 = 0,\\; D_{n+2} = (n+1)(D_n + D_{n+1}) \\quad (n\\in\\mathbb{N}).$$$

Lean4

/-- The number of derangements of an `n`-element set. -/
def numDerangements : ℕ → ℕ
  | 0 => 1
  | 1 => 0
  | n + 2 => (n + 1) * (numDerangements n + numDerangements (n + 1))

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