Commit 2021-09-16 13:26 fdfe782c
View on Github →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.