split(order/monotone): split off order.basic (#9518)

leanprover-community · Oct 3, 2021 · 465508f · 465508f
1 parent c0f7c56
commit 465508f
Show file tree

Hide file tree

Showing 7 changed files with 629 additions and 600 deletions.
diff --git a/src/algebra/order/monoid_lemmas.lean b/src/algebra/order/monoid_lemmas.lean
@@ -3,9 +3,8 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl, Damiano Testa
 -/
-
 import algebra.covariant_and_contravariant
-import order.basic
+import order.monotone
 
 /-!
 # Ordered monoids