File tree Expand file tree Collapse file tree 2 files changed +2
-2
lines changed
Mathlib/Algebra/Order/Positive Expand file tree Collapse file tree 2 files changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -3,8 +3,8 @@ Copyright (c) 2022 Yury Kudryashov. All rights reserved.
33Released under Apache 2.0 license as described in the file LICENSE.
44Authors: Yury Kudryashov
55-/
6- import Mathlib.Algebra.Order.Positive.Ring
76import Mathlib.Algebra.Order.Field.Defs
7+ import Mathlib.Algebra.Order.Positive.Ring
88
99#align_import algebra.order.positive.field from "leanprover-community/mathlib" @"bbeb185db4ccee8ed07dc48449414ebfa39cb821"
1010
Original file line number Diff line number Diff line change 336336 "Mathlib.Algebra.Category.Ring.Basic" :
337337 [" Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso" ],
338338 "Mathlib.Algebra.Algebra.Subalgebra.Order" :
339- [" Mathlib.Algebra.Module.Submodule.Order" ]}}
339+ [" Mathlib.Algebra.Module.Submodule.Order" ]}}
You can’t perform that action at this time.
0 commit comments