Skip to content

Commit

Permalink
automated fixes
Browse files Browse the repository at this point in the history
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
  • Loading branch information
urkud committed Feb 11, 2023
1 parent 90cc033 commit 8813c4f
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 4 deletions.
1 change: 1 addition & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Order/Nonneg/Field.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 8813c4f

Please sign in to comment.