Commit 2023-05-02 10:23 4c8d7858
View on Github →Revert "feat: port Algebra.Order.ToIntervalMod (#2148)" (#3388) This reverts commit 2d0dd3902a4a796d8f38778fec991ab1d4c2a660. The porting comments say "Would be nice to finish leanprover-community/mathlib#17743 first". The commit message says "Might be best to wait". We should wait; there is no urgency to merge this, and no discussion took place that argued against waiting.