mathlib3 documentation

combinatorics.derangements.finite

Derangements on fintypes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 α.
num_derangements n: The number of derangements on an n-element set, defined in a computation- friendly way.
card_derangements_eq_num_derangements: Proof that num_derangements really does compute the number of derangements.
num_derangements_sum: A lemma giving an expression for num_derangements n in terms of factorials.

@[protected, instance]

def derangements.decidable_pred {α : Type u_1} [decidable_eq α] [fintype α] :

decidable_pred (derangements α)

Equations

derangements.decidable_pred = λ (_x : equiv.perm α), fintype.decidable_forall_fintype

@[protected, instance]

def derangements.fintype {α : Type u_1} [decidable_eq α] [fintype α] :

fintype ↥(derangements α)

Equations

derangements.fintype = subtype.fintype (λ (x : equiv.perm α), ∀ (x_1 : α), ¬⇑x x_1 = x_1)

theorem card_derangements_invariant {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq α] [fintype β] [decidable_eq β] (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 num_derangements :

The number of derangements of an n-element set.

Equations

num_derangements (n + 2) = (n + 1) * (num_derangements n + num_derangements n.succ)
num_derangements 1 = 0
num_derangements 0 = 1

@[simp]

theorem num_derangements_zero :

num_derangements 0 = 1

@[simp]

theorem num_derangements_one :

num_derangements 1 = 0

theorem num_derangements_add_two (n : ℕ) :

num_derangements (n + 2) = (n + 1) * (num_derangements n + num_derangements (n + 1))

theorem num_derangements_succ (n : ℕ) :

↑(num_derangements (n + 1)) = (↑n + 1) * ↑(num_derangements n) - (-1) ^ n

theorem card_derangements_fin_eq_num_derangements {n : ℕ} :

fintype.card ↥(derangements (fin n)) = num_derangements n

theorem card_derangements_eq_num_derangements (α : Type u_1) [fintype α] [decidable_eq α] :

fintype.card ↥(derangements α) = num_derangements (fintype.card α)

theorem num_derangements_sum (n : ℕ) :

↑(num_derangements n) = (finset.range (n + 1)).sum (λ (k : ℕ), (-1) ^ k * ↑(k.asc_factorial (n - k)))