Skip to content

Commit a39c314

Browse files
committed
feat: port Algebra.Order.ToIntervalMod (#3952)
1 parent 96a5adb commit a39c314

File tree

2 files changed

+1134
-0
lines changed

2 files changed

+1134
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -259,6 +259,7 @@ import Mathlib.Algebra.Order.Sub.Basic
259259
import Mathlib.Algebra.Order.Sub.Canonical
260260
import Mathlib.Algebra.Order.Sub.Defs
261261
import Mathlib.Algebra.Order.Sub.WithTop
262+
import Mathlib.Algebra.Order.ToIntervalMod
262263
import Mathlib.Algebra.Order.UpperLower
263264
import Mathlib.Algebra.Order.WithZero
264265
import Mathlib.Algebra.Order.ZeroLEOne

0 commit comments

Comments
 (0)