mathlib

fdfe782c - feat(combinatorics/derangements/*): add lemmas about counting derangements (#9089)

feat(combinatorics/derangements/*): add lemmas about counting derangements (#9089) This defines `card_derangements` as the cardinality of the set of derangements of a fintype, and `num_derangements` as a function from N to N, and proves their equality, along with some other lemmas. Context: PR #7526 grew too large and had to be split in half. The first half retained the original PR ID, and this is the second half. This adds back the finite.lean and exponential.lean files. Also, added entries back to 100.yaml. Co-authored-by: Johan Commelin <johan@commelin.net>