diff --git a/Mathlib.lean b/Mathlib.lean index c131d42aee7e9d..111b33d945a3f5 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -153,6 +153,7 @@ import Mathlib.Algebra.Order.Monoid.Units import Mathlib.Algebra.Order.Monoid.WithTop import Mathlib.Algebra.Order.Monoid.WithZero.Basic import Mathlib.Algebra.Order.Monoid.WithZero.Defs +import Mathlib.Algebra.Order.Nonneg.Field import Mathlib.Algebra.Order.Nonneg.Ring import Mathlib.Algebra.Order.Pi import Mathlib.Algebra.Order.Pointwise diff --git a/Mathlib/Algebra/Order/Nonneg/Field.lean b/Mathlib/Algebra/Order/Nonneg/Field.lean index 1e34b53a18d7de..fc023f228e863a 100644 --- a/Mathlib/Algebra/Order/Nonneg/Field.lean +++ b/Mathlib/Algebra/Order/Nonneg/Field.lean @@ -8,10 +8,10 @@ Authors: Floris van Doorn ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.Algebra.Order.Archimedean -import Mathbin.Algebra.Order.Nonneg.Ring -import Mathbin.Algebra.Order.Field.InjSurj -import Mathbin.Algebra.Order.Field.Canonical.Defs +import Mathlib.Algebra.Order.Archimedean +import Mathlib.Algebra.Order.Nonneg.Ring +import Mathlib.Algebra.Order.Field.InjSurj +import Mathlib.Algebra.Order.Field.Canonical.Defs /-! # Semifield structure on the type of nonnegative elements