Documentation

Mathlib.Combinatorics.Derangements.Exponential

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) / n.factorial) Filter.atTop (nhds (-1).exp)