mathlib3 documentation


Derangements on types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Instances for derangements
Instances for derangements
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 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.

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