mathlib

b4a88e2e - feat(data/equiv/derangements/basic): define derangements (#7526)

feat(data/equiv/derangements/basic): define derangements (#7526) This proves two formulas for the number of derangements on _n_ elements, and defines some combinatorial equivalences involving derangements on α and derangements on certain subsets of α. This proves Theorem 88 on Freek's list. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>