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 thatnumDerangements
really does compute the number of derangements.numDerangements_sum
: A lemma giving an expression fornumDerangements n
in terms of factorials.
instance
instFintypeElemPermDerangements
{α : Type u_1}
[DecidableEq α]
[Fintype α]
:
Fintype ↑(derangements α)
Equations
- instFintypeElemPermDerangements = Subtype.fintype fun (x : Equiv.Perm α) => ∀ (x_1 : α), ¬x x_1 = x_1