Skip to content

Commit c640c47

Browse files
committed
fix import
1 parent ae57c9b commit c640c47

File tree

1 file changed

+3
-4
lines changed

1 file changed

+3
-4
lines changed

Mathlib/RingTheory/CohenStructureTheorem.lean

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,16 +11,15 @@ public import Mathlib.Algebra.CharP.MixedCharZero
1111
public import Mathlib.NumberTheory.Padics.RingHoms
1212
public import Mathlib.RingTheory.AdicCompletion.Noetherian
1313
public import Mathlib.RingTheory.AdicCompletion.RingHom
14+
public import Mathlib.RingTheory.AdicCompletion.Topology
1415
public import Mathlib.RingTheory.Flat.Extension
1516
public import Mathlib.RingTheory.Flat.TorsionFree
1617
public import Mathlib.RingTheory.Ideal.Int
18+
public import Mathlib.RingTheory.MvPowerSeries.Evaluation
1719
public import Mathlib.RingTheory.RegularLocalRing.Basic
1820
public import Mathlib.RingTheory.RegularLocalRing.PowerSeries
19-
public import Mathlib.RingTheory.RingHom.Flat
20-
public import Mathlib.Algebra.Algebra.Hom.Rat
21+
public import Mathlib.RingTheory.Smooth.Field
2122
public import Mathlib.RingTheory.Smooth.Quotient
22-
public import Mathlib.RingTheory.MvPowerSeries.Evaluation
23-
public import Mathlib.RingTheory.AdicCompletion.Topology
2423

2524
/-!
2625

0 commit comments

Comments
 (0)