move(order/hom/order): Move from order.hom.lattice (#11601)

Rename `order.hom.lattice` into `order.hom.order` to make space for lattice homomorphisms, as opposed to the lattice of order homomorphisms.
leanprover-community · Jan 22, 2022 · bd3b892 · bd3b892
1 parent 206b56e
commit bd3b892
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 2 deletions.
diff --git a/src/order/fixed_points.lean b/src/order/fixed_points.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Kenny Lau, Yury Kudryashov
 -/
 import dynamics.fixed_points.basic
-import order.hom.lattice
+import order.hom.order
 
 /-!
 # Fixed point construction on complete lattices

diff --git a/src/order/hom/lattice.lean → src/order/hom/order.lean b/src/order/hom/lattice.lean → src/order/hom/order.lean
diff --git a/src/order/omega_complete_partial_order.lean b/src/order/omega_complete_partial_order.lean
@@ -5,7 +5,7 @@ Authors: Simon Hudon
 -/
 import control.monad.basic
 import data.part
-import order.hom.lattice
+import order.hom.order
 import tactic.monotonicity
 import tactic.wlog