move(algebra/order/lattice_group): Move from `algebra.lattice_ordered…

…_group` (#10763) Rename `algebra.lattice_ordered_group` in `algebra/order/lattice_group`.
leanprover-community · Dec 14, 2021 · f070a69 · f070a69
1 parent f727e12
commit f070a69
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 1 deletion.
diff --git a/src/algebra/lattice_ordered_group.lean → src/algebra/order/lattice_group.lean b/src/algebra/lattice_ordered_group.lean → src/algebra/order/lattice_group.lean
diff --git a/src/analysis/normed_space/lattice_ordered_group.lean b/src/analysis/normed_space/lattice_ordered_group.lean
@@ -5,7 +5,7 @@ Authors: Christopher Hoskin
 -/
 import topology.order.lattice
 import analysis.normed.group.basic
-import algebra.lattice_ordered_group
+import algebra.order.lattice_group
 
 /-!
 # Normed lattice ordered groups