mathlib documentation


Derangements on types #

In this file we define derangements α, the set of derangements on a type α.

We also define some equivalences involving various subtypes of perm α and derangements α:

In order to prove the above, we also prove some results about the effect of equiv.remove_none on derangements: remove_none.fiber_none and remove_none.fiber_some.

def derangements (α : Type u_1) :

A permutation is a derangement if it has no fixed points.

def equiv.derangements_congr {α : Type u_1} {β : Type u_2} (e : α β) :

If α is equivalent to β, then derangements α is equivalent to derangements β.

def derangements.subtype_equiv {α : Type u_1} (p : α → Prop) [decidable_pred p] :
(derangements (subtype p)) {f // ∀ (a : α), ¬p a a function.fixed_points f}

Derangements on a subtype are equivalent to permutations on the original type where points are fixed iff they are not in the subtype.


The set of permutations that fix either a or nothing is equivalent to the sum of:

  • derangements on α
  • derangements on α minus a.
def derangements.equiv.remove_none.fiber {α : Type u_1} [decidable_eq α] (a : option α) :

The set of permutations f such that the preimage of (a, f) under equiv.perm.decompose_option is a derangement.


For any a : α, the fiber over some a is the set of permutations where a is the only possible fixed point.

The set of derangements on option α is equivalent to the union over a : α of "permutations with a the only possible fixed point".