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.

instance instDecidablePredPermDerangements {α : Type u_1} [DecidableEq α] [Fintype α] : DecidablePred (derangements α)

Equations

• instDecidablePredPermDerangements x = Fintype.decidableForallFintype

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

Equations

• instFintypeElemPermDerangements = Subtype.fintype fun (x : Equiv.Perm α) => ∀ (x_1 : α), ¬x x_1 = x_1

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.

Equations

• numDerangements 0 = 1
• numDerangements 1 = 0
• numDerangements (Nat.succ (Nat.succ n)) = (n + 1) * (numDerangements n + numDerangements (n + 1))

@[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) = Finset.sum (Finset.range (n + 1)) fun (k : ℕ) => (-1) ^ k * ↑(Nat.ascFactorial (k + 1) (n - k))