Documentation

Mathlib.Combinatorics.Derangements.Finite

Derangements on fintypes #

This file contains lemmas that describe the cardinality of derangements α when α is a fintype.

Main definitions #

The number of derangements of an n-element set.

Equations
Instances For
    theorem numDerangements_succ (n : ) :
    ↑(numDerangements (n + 1)) = (n + 1) * ↑(numDerangements n) - (-1) ^ n
    theorem numDerangements_sum (n : ) :
    ↑(numDerangements n) = Finset.sum (Finset.range (n + 1)) fun k => (-1) ^ k * ↑(Nat.ascFactorial k (n - k))