chore (Order.OmegaCompletePartialOrder): avoid importing ordered alge…

…bra (#14338) This seems to be a redundant import.
leanprover-community · Jul 1, 2024 · 29dcec0 · 29dcec0
1 parent aa30cf9
commit 29dcec0
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/Mathlib/Order/OmegaCompletePartialOrder.lean b/Mathlib/Order/OmegaCompletePartialOrder.lean
@@ -7,7 +7,6 @@ import Mathlib.Control.Monad.Basic
 import Mathlib.Data.Part
 import Mathlib.Order.Chain
 import Mathlib.Order.Hom.Order
-import Mathlib.Algebra.Order.Ring.Nat
 
 #align_import order.omega_complete_partial_order from "leanprover-community/mathlib"@"92ca63f0fb391a9ca5f22d2409a6080e786d99f7"