Theorems · Theorem · combinatorics

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)))

Defined in: Mathlib.Combinatorics.Derangements.Finite
Cited by: 1 results in Mathlib
Foundations: Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites21

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Set.Elemstatement and proof · cited by 7,166
Finset.univproof · cited by 3,473
Compl.complproof · cited by 2,925
Finset.sum_congrproof · cited by 2,323
Fintype.cardstatement and proof · cited by 1,386
Equiv.Permstatement · cited by 1,375
mul_addproof · cited by 413
nsmul_eq_mulproof · cited by 369
Fintype.card_finproof · cited by 270
Finset.sum_constproof · cited by 254
add_tsub_cancel_rightproof · cited by 172
Fintype.card_congrproof · cited by 67

Cited by1

Results whose statement or proof uses this declaration.

card_derangements_fin_eq_numDerangementsproof · cited by 1