Skip to content

Commit e38fc33

Browse files
committed
fix import
1 parent 93fc39f commit e38fc33

File tree

1 file changed

+3
-11
lines changed

1 file changed

+3
-11
lines changed

Mathlib/FieldTheory/TranscendentalSeparable.lean

Lines changed: 3 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -5,19 +5,11 @@ Authors: Nailin Guan
55
-/
66
module
77

8-
public import Mathlib.RingTheory.Flat.Basic
9-
public import Mathlib.RingTheory.TensorProduct.DirectLimitFG
10-
public import Mathlib.FieldTheory.Perfect
11-
public import Mathlib.FieldTheory.Separable
12-
public import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
13-
public import Mathlib.RingTheory.Ideal.MinimalPrime.Basic
14-
public import Mathlib.RingTheory.Localization.AtPrime.Basic
15-
public import Mathlib.RingTheory.LocalProperties.Reduced
16-
public import Mathlib.RingTheory.TensorProduct.Pi
8+
public import Mathlib.FieldTheory.SeparablyGenerated
179
public import Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian
18-
public import Mathlib.FieldTheory.PrimitiveElement
10+
public import Mathlib.RingTheory.LocalProperties.Reduced
1911
public import Mathlib.RingTheory.Nilpotent.GeometricallyReduced
20-
public import Mathlib.FieldTheory.SeparablyGenerated
12+
public import Mathlib.RingTheory.TensorProduct.Pi
2113

2214
/-!
2315
# Transcendental separable extensions

0 commit comments

Comments
 (0)