Commit 2021-09-16 13:26 fdfe782c

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.