mathlib documentation

combinatorics.derangements.finite

Derangements on fintypes #

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

Main definitions #

@[instance]
def derangements.fintype {α : Type u_1} [decidable_eq α] [fintype α] :
Equations
def num_derangements  :

The number of derangements of an n-element set.

Equations
@[simp]
theorem num_derangements_succ (n : ) :
(num_derangements (n + 1)) = (n + 1) * (num_derangements n) - (-1) ^ n
theorem num_derangements_sum (n : ) :
(num_derangements n) = ∑ (k : ) in finset.range (n + 1), ((-1) ^ k) * (k.asc_factorial (n - k))