# Documentation

Mathlib.Combinatorics.Derangements.Finite

# Derangements on fintypes #

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

# Main definitions #

• card_derangements_invariant: A lemma stating that the number of derangements on a type α depends only on the cardinality of α.
• numDerangements n: The number of derangements on an n-element set, defined in a computation- friendly way.
• card_derangements_eq_numDerangements: Proof that numDerangements really does compute the number of derangements.
• numDerangements_sum: A lemma giving an expression for numDerangements n in terms of factorials.
instance instDecidablePredPermDerangements {α : Type u_1} [] [] :
instance instFintypeElemPermDerangements {α : Type u_1} [] [] :
Fintype ↑()
theorem card_derangements_invariant {α : Type u_2} {β : Type u_3} [] [] [] [] (h : ) :

The number of derangements of an n-element set.

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