mathlib3documentation

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]
Equations
@[protected, instance]
def derangements.fintype {α : Type u_1} [decidable_eq α] [fintype α] :
Equations
theorem card_derangements_invariant {α : Type u_1} {β : Type u_2} [fintype α] [decidable_eq α] [fintype β] [decidable_eq β] (h : = ) :

The number of derangements of an n-element set.

Equations
@[simp]
theorem num_derangements_zero  :
@[simp]
theorem num_derangements_one  :
theorem num_derangements_add_two (n : ) :
num_derangements (n + 2) = (n + 1) * + num_derangements (n + 1))
theorem num_derangements_succ (n : ) :
(num_derangements (n + 1)) = (n + 1) * - (-1) ^ n
theorem num_derangements_sum (n : ) :
= (finset.range (n + 1)).sum (λ (k : ), (-1) ^ k * (k.asc_factorial (n - k)))