Move files

leanprover-community · Oct 19, 2024 · fe9b272 · fe9b272
1 parent 069f950
commit fe9b272
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 2 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1025,7 +1025,6 @@ import Mathlib.Analysis.Calculus.SmoothSeries
 import Mathlib.Analysis.Calculus.TangentCone
 import Mathlib.Analysis.Calculus.Taylor
 import Mathlib.Analysis.Calculus.UniformLimitsDeriv
-import Mathlib.Analysis.CauchyBound
 import Mathlib.Analysis.Complex.AbelLimit
 import Mathlib.Analysis.Complex.AbsMax
 import Mathlib.Analysis.Complex.Angle
@@ -1273,6 +1272,8 @@ import Mathlib.Analysis.ODE.PicardLindelof
 import Mathlib.Analysis.Oscillation
 import Mathlib.Analysis.PSeries
 import Mathlib.Analysis.PSeriesComplex
+import Mathlib.Analysis.Polynomial.Basic
+import Mathlib.Analysis.Polynomial.CauchyBound
 import Mathlib.Analysis.Quaternion
 import Mathlib.Analysis.RCLike.Basic
 import Mathlib.Analysis.RCLike.Lemmas
@@ -1315,7 +1316,6 @@ import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
 import Mathlib.Analysis.SpecialFunctions.NonIntegrable
 import Mathlib.Analysis.SpecialFunctions.PolarCoord
 import Mathlib.Analysis.SpecialFunctions.PolynomialExp
-import Mathlib.Analysis.SpecialFunctions.Polynomials
 import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
 import Mathlib.Analysis.SpecialFunctions.Pow.Complex
 import Mathlib.Analysis.SpecialFunctions.Pow.Continuity

diff --git a/...nalysis/SpecialFunctions/Polynomials.lean → Mathlib/Analysis/Polynomial/Basic.lean b/...nalysis/SpecialFunctions/Polynomials.lean → Mathlib/Analysis/Polynomial/Basic.lean
diff --git a/Mathlib/Analysis/CauchyBound.lean → Mathlib/Analysis/Polynomial/CauchyBound.lean b/Mathlib/Analysis/CauchyBound.lean → Mathlib/Analysis/Polynomial/CauchyBound.lean