# mathlib3documentation

combinatorics.derangements.basic

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

• derangements_option_equiv_sigma_at_most_one_fixed_point: An equivalence between derangements (option α) and the sigma-type Σ a : α, {f : perm α // fixed_points f ⊆ a}.
• derangements_recursion_equiv: 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.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.

Equations
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 β.

Equations
@[protected]
def derangements.subtype_equiv {α : Type u_1} (p : α Prop)  :
(derangements (subtype p)) {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.

Equations

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

• derangements on α
• derangements on α minus a.
Equations

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

Equations
• = {f : | (a, f)
theorem derangements.equiv.remove_none.fiber_some {α : Type u_1} [decidable_eq α] (a : α) :
= {f : | {a}}

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

Equations

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

Equations