# Documentation

Mathlib.Combinatorics.Derangements.Basic

# 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 α:

• derangementsOptionEquivSigmaAtMostOneFixedPoint: An equivalence between derangements (Option α) and the sigma-type Σ a : α, {f : Perm α // fixed_points f ⊆ a}.
• derangementsRecursionEquiv: An equivalence between derangements (Option α) and the sigma-type Σ a : α, (derangements (({a}ᶜ : Set α) : Type*) ⊕ derangements α) which is later used to inductively count the number of derangements.

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

def derangements (α : Type u_1) :
Set ()

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

Instances For
def Equiv.derangementsCongr {α : Type u_1} {β : Type u_2} (e : α β) :
↑() ↑()

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

Instances For
def derangements.subtypeEquiv {α : Type u_1} (p : αProp) [] :
↑() { f // ∀ (a : α), ¬p a }

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

Instances For
def derangements.atMostOneFixedPointEquivSum_derangements {α : Type u_1} [] (a : α) :
{ f // {a} } ↑(derangements {a}) ↑()

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

• derangements on α
• derangements on α minus a.
Instances For
def derangements.Equiv.RemoveNone.fiber {α : Type u_1} [] (a : ) :
Set ()

The set of permutations f such that the preimage of (a, f) under Equiv.Perm.decomposeOption is a derangement.

Instances For
theorem derangements.Equiv.RemoveNone.mem_fiber {α : Type u_1} [] (a : ) (f : ) :
F, F F none = a
theorem derangements.Equiv.RemoveNone.fiber_some {α : Type u_1} [] (a : α) :
= {f | {a}}

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

def derangements.derangementsOptionEquivSigmaAtMostOneFixedPoint {α : Type u_1} [] :
↑() (a : α) × {f | {a}}

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

Instances For
def derangements.derangementsRecursionEquiv {α : Type u_1} [] :
↑() (a : α) × (↑(derangements {a}) ↑())

The set of derangements on Option α is equivalent to the union over all a : α of "derangements on α ⊕ derangements on {a}ᶜ".

Instances For