chore: drop some unnecessary imports (#3869)

leanprover-community · May 10, 2023 · ee97f52 · ee97f52
1 parent 9912e05
commit ee97f52
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 4 deletions.
diff --git a/Mathlib/Algebra/Order/AbsoluteValue.lean b/Mathlib/Algebra/Order/AbsoluteValue.lean
@@ -11,8 +11,6 @@ Authors: Mario Carneiro, Anne Baanen
 import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 import Mathlib.Algebra.Order.Field.Defs
 import Mathlib.Algebra.Order.Hom.Basic
-import Mathlib.Algebra.Order.Ring.Abs
-import Mathlib.Algebra.Ring.Commute
 import Mathlib.Algebra.Ring.Regular
 
 /-!

diff --git a/Mathlib/Algebra/Order/Hom/Basic.lean b/Mathlib/Algebra/Order/Hom/Basic.lean
@@ -9,8 +9,7 @@ Authors: Yaël Dillies
 ! if you have ported upstream changes.
 -/
 
-import Mathlib.Tactic.Positivity
-import Mathlib.Data.FunLike.Basic
+import Mathlib.Algebra.GroupPower.Order
 
 /-!
 # Algebraic order homomorphism classes