mathlib documentation

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 num_derangements_tendsto_inv_e.