feat: port Order.Circular (#1489)

Co-authored-by: thorimur <68410468+thorimur@users.noreply.github.com>
leanprover-community · Jan 12, 2023 · 90a54f4 · 90a54f4
1 parent b35d023
commit 90a54f4
Show file tree

Hide file tree

Showing 2 changed files with 502 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -487,6 +487,7 @@ import Mathlib.Order.BoundedOrder
 import Mathlib.Order.Bounds.Basic
 import Mathlib.Order.Bounds.OrderIso
 import Mathlib.Order.Chain
+import Mathlib.Order.Circular
 import Mathlib.Order.Closure
 import Mathlib.Order.Compare
 import Mathlib.Order.CompleteBooleanAlgebra