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 that numDerangements really does compute the number of derangements.
• numDerangements_sum: A lemma giving an expression for numDerangements n in terms of factorials.

@[implicit_reducible]

instance instDecidablePredPermMemSetDerangements {α : Type u_1} [DecidableEq α] [Fintype α] : DecidablePred fun (x : Equiv.Perm α) => x ∈ derangements α

@[implicit_reducible]

instance instFintypeElemPermDerangements {α : Type u_1} [DecidableEq α] [Fintype α] : Fintype ↑(derangements α)

theorem card_derangements_invariant {α : Type u_2} {β : Type u_3} [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (h : Fintype.card α = Fintype.card β) : Fintype.card ↑(derangements α) = Fintype.card ↑(derangements β)

theorem card_derangements_fin_add_two (n : ℕ) : Fintype.card ↑(derangements (Fin (n + 2))) = (n + 1) * Fintype.card ↑(derangements (Fin n)) + (n + 1) * Fintype.card ↑(derangements (Fin (n + 1)))

def numDerangements : ℕ → ℕ

The number of derangements of an n-element set.

@[simp]

theorem numDerangements_zero : numDerangements 0 = 1

@[simp]

theorem numDerangements_one : numDerangements 1 = 0

theorem numDerangements_add_two (n : ℕ) : numDerangements (n + 2) = (n + 1) * (numDerangements n + numDerangements (n + 1))

theorem numDerangements_succ (n : ℕ) : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n

theorem card_derangements_fin_eq_numDerangements {n : ℕ} : Fintype.card ↑(derangements (Fin n)) = numDerangements n

theorem card_derangements_eq_numDerangements (α : Type u_2) [Fintype α] [DecidableEq α] : Fintype.card ↑(derangements α) = numDerangements (Fintype.card α)

theorem numDerangements_sum (n : ℕ) : ↑(numDerangements n) = ∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))