diff --git a/Mathlib/Topology/Algebra/Field.lean b/Mathlib/Topology/Algebra/Field.lean index 7e78ef983d7f6a..cc34c6223561e6 100644 --- a/Mathlib/Topology/Algebra/Field.lean +++ b/Mathlib/Topology/Algebra/Field.lean @@ -5,10 +5,10 @@ Authors: Patrick Massot, Kim Morrison -/ import Mathlib.Algebra.Field.Subfield.Basic import Mathlib.Algebra.GroupWithZero.Divisibility +import Mathlib.Algebra.Order.Group.Pointwise.Interval import Mathlib.Topology.Algebra.GroupWithZero import Mathlib.Topology.Algebra.Ring.Basic import Mathlib.Topology.Order.LocalExtr -import Mathlib.Data.Set.Pointwise.Interval /-! # Topological fields