Commit 2023-04-11 09:57 2d0dd390
View on Github →feat: port Algebra.Order.ToIntervalMod (#2148) Only now realized that this is part of an ongoing project within mathlib3, see https://github.com/leanprover-community/mathlib/pull/17743. Might be best to wait.