shake

leanprover-community · Oct 25, 2024 · 7d83cff · 7d83cff
1 parent dbb9357
commit 7d83cff
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 6 deletions.
diff --git 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
@@ -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
@@ -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