Commit 2023-03-23 16:06 19cc4324

View on Github →

feat: Port/Combinatorics.Derangements.Basic (#2530)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Derangements/Basic.lean

added def Equiv.derangementsCongr

added def derangements.Equiv.RemoveNone.fiber

added theorem derangements.Equiv.RemoveNone.fiber_none

added theorem derangements.Equiv.RemoveNone.fiber_some

added theorem derangements.Equiv.RemoveNone.mem_fiber

added def derangements.atMostOneFixedPointEquivSum_derangements

added def derangements.derangementsOptionEquivSigmaAtMostOneFixedPoint

added def derangements.derangementsRecursionEquiv

added def derangements

added theorem mem_derangements_iff_fixedPoints_eq_empty

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Logic/Equiv/Basic.lean

modified def Equiv.subtypeSubtypeEquivSubtypeInter