Derangement exponential series

This file proves that the probability of a permutation on n elements being a derangement is 1/e. The specific lemma is numDerangements_tendsto_inv_e.

theorem numDerangements_tendsto_inv_e : Filter.Tendsto (fun (n : ℕ) => ↑(numDerangements n) / ↑(Nat.factorial n)) Filter.atTop (nhds (Real.exp (-1)))