diff --git a/src/algebra/lattice_ordered_group.lean b/src/algebra/order/lattice_group.lean similarity index 100% rename from src/algebra/lattice_ordered_group.lean rename to 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 index 47eec1ea184da..91608402a33a3 100644 --- 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