Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-08 08:23 b4a88e2e

View on Github →

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.

Estimated changes