From 8813c4f21f555dd6eae2730e586b9733b6ef49ab Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Fri, 10 Feb 2023 23:33:58 -0600 Subject: [PATCH] automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean --- Mathlib.lean | 1 + Mathlib/Algebra/Order/Nonneg/Field.lean | 8 ++++---- 2 files changed, 5 insertions(+), 4 deletions(-) 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