diff --git a/FltRegular/NumberTheory/Finrank.lean b/FltRegular/NumberTheory/Finrank.lean
index 5e430d78..58af4510 100644
--- a/FltRegular/NumberTheory/Finrank.lean
+++ b/FltRegular/NumberTheory/Finrank.lean
@@ -1,8 +1,4 @@
-import Mathlib.LinearAlgebra.Dimension.Constructions
-import Mathlib.LinearAlgebra.Dimension.Finite
-import Mathlib.Algebra.Module.Torsion
-import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
-import Mathlib.LinearAlgebra.Dimension.Localization
+import Mathlib.GroupTheory.Torsion
 
 open Module
 section
diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean
index a244c916..864567ef 100644
--- a/FltRegular/NumberTheory/Hilbert92.lean
+++ b/FltRegular/NumberTheory/Hilbert92.lean
@@ -7,6 +7,7 @@ import Mathlib.GroupTheory.FiniteAbelian
 import Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
 import Mathlib.Order.CompletePartialOrder
 import Mathlib.RingTheory.Henselian
+import FltRegular.NumberTheory.Finrank
 
 open scoped NumberField nonZeroDivisors
 open FiniteDimensional NumberField
diff --git a/FltRegular/NumberTheory/SystemOfUnits.lean b/FltRegular/NumberTheory/SystemOfUnits.lean
index 82bd4a61..1c262d71 100644
--- a/FltRegular/NumberTheory/SystemOfUnits.lean
+++ b/FltRegular/NumberTheory/SystemOfUnits.lean
@@ -1,7 +1,7 @@
 import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
 import FltRegular.NumberTheory.CyclotomicRing
-import FltRegular.NumberTheory.Finrank
 import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
+import Mathlib.LinearAlgebra.Dimension.Localization
 
 open FiniteDimensional
 open NumberField