Commit 2023-03-27 11:56 1b816f73

View on Github →

feat: port Combinatorics.Derangements.Finite (#3102)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Derangements/Finite.lean

added theorem card_derangements_eq_numDerangements

added theorem card_derangements_fin_add_two

added theorem card_derangements_fin_eq_numDerangements

added theorem card_derangements_invariant

added def numDerangements

added theorem numDerangements_add_two

added theorem numDerangements_one

added theorem numDerangements_succ

added theorem numDerangements_sum

added theorem numDerangements_zero