chore: move integralNormalization to RingTheory/Polynomial (#6215)

A similar file `ScaleRoots` is also in `RingTheory/Polynomial`.
leanprover-community · Jul 28, 2023 · 45bc825 · 45bc825
1 parent 5c3c589
commit 45bc825
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 2 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1664,7 +1664,6 @@ import Mathlib.Data.Polynomial.HasseDeriv
 import Mathlib.Data.Polynomial.Identities
 import Mathlib.Data.Polynomial.Induction
 import Mathlib.Data.Polynomial.Inductions
-import Mathlib.Data.Polynomial.IntegralNormalization
 import Mathlib.Data.Polynomial.Laurent
 import Mathlib.Data.Polynomial.Lifts
 import Mathlib.Data.Polynomial.Mirror
@@ -2818,6 +2817,7 @@ import Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
 import Mathlib.RingTheory.Polynomial.GaussLemma
 import Mathlib.RingTheory.Polynomial.Hermite.Basic
 import Mathlib.RingTheory.Polynomial.Hermite.Gaussian
+import Mathlib.RingTheory.Polynomial.IntegralNormalization
 import Mathlib.RingTheory.Polynomial.Opposites
 import Mathlib.RingTheory.Polynomial.Pochhammer
 import Mathlib.RingTheory.Polynomial.Quotient

diff --git a/Mathlib/RingTheory/Algebraic.lean b/Mathlib/RingTheory/Algebraic.lean
@@ -5,7 +5,7 @@ Authors: Johan Commelin
 -/
 import Mathlib.LinearAlgebra.FiniteDimensional
 import Mathlib.RingTheory.IntegralClosure
-import Mathlib.Data.Polynomial.IntegralNormalization
+import Mathlib.RingTheory.Polynomial.IntegralNormalization
 
 #align_import ring_theory.algebraic from "leanprover-community/mathlib"@"2196ab363eb097c008d4497125e0dde23fb36db2"
 

diff --git a/...ata/Polynomial/IntegralNormalization.lean → ...ory/Polynomial/IntegralNormalization.lean b/...ata/Polynomial/IntegralNormalization.lean → ...ory/Polynomial/IntegralNormalization.lean