chore(Analysis/{NormedSpace,Normed/Module}): migrate all remaining files (#30281)

j-loreaux · j-loreaux · commit 312eeb7c9495 · 2025-11-21T13:53:10.000Z
closes #28698
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1905,21 +1905,35 @@ public import Mathlib.Analysis.Normed.Lp.PiLp
 public import Mathlib.Analysis.Normed.Lp.ProdLp
 public import Mathlib.Analysis.Normed.Lp.WithLp
 public import Mathlib.Analysis.Normed.Lp.lpSpace
+public import Mathlib.Analysis.Normed.Module.Alternating.Basic
+public import Mathlib.Analysis.Normed.Module.Alternating.Curry
+public import Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
 public import Mathlib.Analysis.Normed.Module.Ball.Action
 public import Mathlib.Analysis.Normed.Module.Ball.Homeomorph
 public import Mathlib.Analysis.Normed.Module.Ball.Pointwise
 public import Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
 public import Mathlib.Analysis.Normed.Module.Basic
 public import Mathlib.Analysis.Normed.Module.Complemented
 public import Mathlib.Analysis.Normed.Module.Completion
+public import Mathlib.Analysis.Normed.Module.Connected
 public import Mathlib.Analysis.Normed.Module.Convex
 public import Mathlib.Analysis.Normed.Module.Dual
+public import Mathlib.Analysis.Normed.Module.ENormedSpace
+public import Mathlib.Analysis.Normed.Module.Extr
 public import Mathlib.Analysis.Normed.Module.FiniteDimension
 public import Mathlib.Analysis.Normed.Module.HahnBanach
+public import Mathlib.Analysis.Normed.Module.MStructure
+public import Mathlib.Analysis.Normed.Module.Multilinear.Basic
+public import Mathlib.Analysis.Normed.Module.Multilinear.Curry
+public import Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
+public import Mathlib.Analysis.Normed.Module.Normalize
+public import Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
+public import Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
 public import Mathlib.Analysis.Normed.Module.RCLike.Basic
 public import Mathlib.Analysis.Normed.Module.RCLike.Extend
 public import Mathlib.Analysis.Normed.Module.RCLike.Real
 public import Mathlib.Analysis.Normed.Module.Ray
+public import Mathlib.Analysis.Normed.Module.RieszLemma
 public import Mathlib.Analysis.Normed.Module.Span
 public import Mathlib.Analysis.Normed.Module.WeakDual
 public import Mathlib.Analysis.Normed.MulAction
@@ -1962,25 +1976,14 @@ public import Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
 public import Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
 public import Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
 public import Mathlib.Analysis.Normed.Unbundled.SpectralNorm
-public import Mathlib.Analysis.NormedSpace.Alternating.Basic
-public import Mathlib.Analysis.NormedSpace.Alternating.Curry
-public import Mathlib.Analysis.NormedSpace.Alternating.Uncurry.Fin
 public import Mathlib.Analysis.NormedSpace.BallAction
 public import Mathlib.Analysis.NormedSpace.ConformalLinearMap
-public import Mathlib.Analysis.NormedSpace.Connected
 public import Mathlib.Analysis.NormedSpace.DualNumber
-public import Mathlib.Analysis.NormedSpace.ENormedSpace
 public import Mathlib.Analysis.NormedSpace.Extend
-public import Mathlib.Analysis.NormedSpace.Extr
 public import Mathlib.Analysis.NormedSpace.FunctionSeries
 public import Mathlib.Analysis.NormedSpace.HomeomorphBall
 public import Mathlib.Analysis.NormedSpace.IndicatorFunction
 public import Mathlib.Analysis.NormedSpace.Int
-public import Mathlib.Analysis.NormedSpace.MStructure
-public import Mathlib.Analysis.NormedSpace.Multilinear.Basic
-public import Mathlib.Analysis.NormedSpace.Multilinear.Curry
-public import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
-public import Mathlib.Analysis.NormedSpace.Normalize
 public import Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics
 public import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic
 public import Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear
@@ -1989,12 +1992,9 @@ public import Mathlib.Analysis.NormedSpace.OperatorNorm.Mul
 public import Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm
 public import Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace
 public import Mathlib.Analysis.NormedSpace.OperatorNorm.Prod
-public import Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm
-public import Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm
 public import Mathlib.Analysis.NormedSpace.Pointwise
 public import Mathlib.Analysis.NormedSpace.RCLike
 public import Mathlib.Analysis.NormedSpace.Real
-public import Mathlib.Analysis.NormedSpace.RieszLemma
 public import Mathlib.Analysis.NormedSpace.SphereNormEquiv
 public import Mathlib.Analysis.ODE.Gronwall
 public import Mathlib.Analysis.ODE.PicardLindelof
diff --git a/Mathlib/Analysis/CStarAlgebra/Unitary/Span.lean b/Mathlib/Analysis/CStarAlgebra/Unitary/Span.lean
@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
 public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
-public import Mathlib.Analysis.NormedSpace.Normalize
+public import Mathlib.Analysis.Normed.Module.Normalize
 
 /-! # Unitary elements span C⋆-algebras
 
diff --git a/Mathlib/Analysis/Calculus/DifferentialForm/Basic.lean b/Mathlib/Analysis/Calculus/DifferentialForm/Basic.lean
@@ -5,7 +5,7 @@ Authors: Yury G. Kudryashov, Sam Lindauer
 -/
 module
 
-public import Mathlib.Analysis.NormedSpace.Alternating.Uncurry.Fin
+public import Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin
 public import Mathlib.Analysis.Calculus.FDeriv.Symmetric
 public import Mathlib.Analysis.Calculus.FDeriv.CompCLM
 
diff --git a/Mathlib/Analysis/Calculus/FDeriv/CompCLM.lean b/Mathlib/Analysis/Calculus/FDeriv/CompCLM.lean
@@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Sébastien Gouëzel, Yury Kudryashov
 module
 
 public import Mathlib.Analysis.Calculus.FDeriv.Bilinear
-public import Mathlib.Analysis.NormedSpace.Alternating.Basic
+public import Mathlib.Analysis.Normed.Module.Alternating.Basic
 
 /-!
 # Multiplicative operations on derivatives
diff --git a/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean b/Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
@@ -5,7 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 module
 
-public import Mathlib.Analysis.NormedSpace.Multilinear.Curry
+public import Mathlib.Analysis.Normed.Module.Multilinear.Curry
 
 /-!
 # Formal multilinear series
diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/ConvergenceOnBall.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/ConvergenceOnBall.lean
@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Analysis.Analytic.Uniqueness
 public import Mathlib.Analysis.Calculus.IteratedDeriv.Defs
-public import Mathlib.Analysis.NormedSpace.Connected
+public import Mathlib.Analysis.Normed.Module.Connected
 public import Mathlib.Analysis.RCLike.Basic
 
 /-!
diff --git a/Mathlib/Analysis/Complex/AbsMax.lean b/Mathlib/Analysis/Complex/AbsMax.lean
@@ -8,7 +8,7 @@ module
 public import Mathlib.Analysis.Complex.CauchyIntegral
 public import Mathlib.Analysis.InnerProductSpace.Convex
 public import Mathlib.Analysis.Normed.Affine.AddTorsor
-public import Mathlib.Analysis.NormedSpace.Extr
+public import Mathlib.Analysis.Normed.Module.Extr
 public import Mathlib.LinearAlgebra.Complex.FiniteDimensional
 public import Mathlib.Topology.Order.ExtrClosure
 
diff --git a/Mathlib/Analysis/Convex/AmpleSet.lean b/Mathlib/Analysis/Convex/AmpleSet.lean
@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Algebra.CharP.Invertible
 public import Mathlib.Analysis.Normed.Module.Convex
-public import Mathlib.Analysis.NormedSpace.Connected
+public import Mathlib.Analysis.Normed.Module.Connected
 public import Mathlib.Topology.Algebra.ContinuousAffineEquiv
 
 /-!
diff --git a/Mathlib/Analysis/Normed/Module/Alternating/Basic.lean b/Mathlib/Analysis/Normed/Module/Alternating/Basic.lean
@@ -6,7 +6,7 @@ Authors: Sébastien Gouëzel, Yury Kudryashov, Heather Macbeth, Patrick Massot
 module
 
 public import Mathlib.Topology.Algebra.Module.Alternating.Topology
-public import Mathlib.Analysis.NormedSpace.Multilinear.Basic
+public import Mathlib.Analysis.Normed.Module.Multilinear.Basic
 
 /-!
 # Operator norm on the space of continuous alternating maps
diff --git a/Mathlib/Analysis/Normed/Module/Alternating/Curry.lean b/Mathlib/Analysis/Normed/Module/Alternating/Curry.lean
@@ -6,8 +6,8 @@ Authors: Yury Kudryashov, Eric Wieser
 module
 
 public import Mathlib.LinearAlgebra.Alternating.Curry
-public import Mathlib.Analysis.NormedSpace.Alternating.Basic
-public import Mathlib.Analysis.NormedSpace.Multilinear.Curry
+public import Mathlib.Analysis.Normed.Module.Alternating.Basic
+public import Mathlib.Analysis.Normed.Module.Multilinear.Curry
 
 /-!
 # Currying continuous alternating forms
diff --git a/Mathlib/Analysis/Normed/Module/Alternating/Uncurry/Fin.lean b/Mathlib/Analysis/Normed/Module/Alternating/Uncurry/Fin.lean
@@ -5,7 +5,7 @@ Authors: Yury Kudryashov
 -/
 module
 
-public import Mathlib.Analysis.NormedSpace.Alternating.Curry
+public import Mathlib.Analysis.Normed.Module.Alternating.Curry
 public import Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
 
 /-!
diff --git a/Mathlib/Analysis/Normed/Module/Connected.lean b/Mathlib/Analysis/Normed/Module/Connected.lean
diff --git a/Mathlib/Analysis/Normed/Module/ENormedSpace.lean b/Mathlib/Analysis/Normed/Module/ENormedSpace.lean
diff --git a/Mathlib/Analysis/Normed/Module/Extr.lean b/Mathlib/Analysis/Normed/Module/Extr.lean
diff --git a/Mathlib/Analysis/Normed/Module/FiniteDimension.lean b/Mathlib/Analysis/Normed/Module/FiniteDimension.lean
@@ -9,7 +9,7 @@ public import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
 public import Mathlib.Analysis.Normed.Group.Lemmas
 public import Mathlib.Analysis.Normed.Affine.Isometry
 public import Mathlib.Analysis.Normed.Operator.NormedSpace
-public import Mathlib.Analysis.NormedSpace.RieszLemma
+public import Mathlib.Analysis.Normed.Module.RieszLemma
 public import Mathlib.Analysis.Normed.Module.Ball.Pointwise
 public import Mathlib.Analysis.SpecificLimits.Normed
 public import Mathlib.Logic.Encodable.Pi
diff --git a/Mathlib/Analysis/Normed/Module/MStructure.lean b/Mathlib/Analysis/Normed/Module/MStructure.lean
diff --git a/Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean b/Mathlib/Analysis/Normed/Module/Multilinear/Basic.lean
diff --git a/Mathlib/Analysis/Normed/Module/Multilinear/Curry.lean b/Mathlib/Analysis/Normed/Module/Multilinear/Curry.lean
@@ -5,7 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 module
 
-public import Mathlib.Analysis.NormedSpace.Multilinear.Basic
+public import Mathlib.Analysis.Normed.Module.Multilinear.Basic
 public import Mathlib.LinearAlgebra.Multilinear.Curry
 
 /-!
diff --git a/Mathlib/Analysis/Normed/Module/MultipliableUniformlyOn.lean b/Mathlib/Analysis/Normed/Module/MultipliableUniformlyOn.lean
diff --git a/Mathlib/Analysis/Normed/Module/Normalize.lean b/Mathlib/Analysis/Normed/Module/Normalize.lean
diff --git a/Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean b/Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean
@@ -5,7 +5,7 @@ Authors: Sophie Morel
 -/
 module
 
-public import Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm
+public import Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
 public import Mathlib.LinearAlgebra.Isomorphisms
 
 /-!
diff --git a/Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean b/Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean
@@ -5,7 +5,7 @@ Authors: Sophie Morel
 -/
 module
 
-public import Mathlib.Analysis.NormedSpace.Multilinear.Basic
+public import Mathlib.Analysis.Normed.Module.Multilinear.Basic
 public import Mathlib.LinearAlgebra.PiTensorProduct
 
 /-!
diff --git a/Mathlib/Analysis/Normed/Module/RieszLemma.lean b/Mathlib/Analysis/Normed/Module/RieszLemma.lean
diff --git a/Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean b/Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean
@@ -5,7 +5,7 @@ Authors: Patrick Massot, Johannes Hölzl
 -/
 module
 
-public import Mathlib.Analysis.NormedSpace.Multilinear.Basic
+public import Mathlib.Analysis.Normed.Module.Multilinear.Basic
 public import Mathlib.Analysis.Normed.Ring.Units
 public import Mathlib.Analysis.Normed.Operator.Mul
 
diff --git a/Mathlib/Analysis/Normed/Operator/CompleteCodomain.lean b/Mathlib/Analysis/Normed/Operator/CompleteCodomain.lean
@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Algebra.Central.Defs
 public import Mathlib.Analysis.LocallyConvex.SeparatingDual
-public import Mathlib.Analysis.NormedSpace.Multilinear.Basic
+public import Mathlib.Analysis.Normed.Module.Multilinear.Basic
 public import Mathlib.LinearAlgebra.Dual.Lemmas
 
 /-! # Completeness of spaces of linear and multilinear maps
diff --git a/Mathlib/Analysis/SpecialFunctions/Integrability/LogMeromorphic.lean b/Mathlib/Analysis/SpecialFunctions/Integrability/LogMeromorphic.lean
@@ -6,7 +6,7 @@ Authors: Stefan Kebekus
 module
 
 public import Mathlib.Analysis.Meromorphic.FactorizedRational
-public import Mathlib.Analysis.NormedSpace.Connected
+public import Mathlib.Analysis.Normed.Module.Connected
 public import Mathlib.Analysis.SpecialFunctions.Integrability.Basic
 public import Mathlib.Analysis.SpecialFunctions.Log.PosLog
 public import Mathlib.LinearAlgebra.Complex.FiniteDimensional
diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean
@@ -11,7 +11,7 @@ public import Mathlib.Analysis.Complex.IntegerCompl
 public import Mathlib.Analysis.Complex.LocallyUniformLimit
 public import Mathlib.Analysis.PSeries
 public import Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
-public import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
+public import Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
 public import Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
 
diff --git a/Mathlib/Geometry/Euclidean/SignedDist.lean b/Mathlib/Geometry/Euclidean/SignedDist.lean
@@ -6,7 +6,7 @@ Authors: Joseph Myers
 module
 
 public import Mathlib.Geometry.Euclidean.Projection
-public import Mathlib.Analysis.NormedSpace.Normalize
+public import Mathlib.Analysis.Normed.Module.Normalize
 
 /-!
 # Signed distance to an affine subspace in a Euclidean space.
diff --git a/Mathlib/NumberTheory/LSeries/ZMod.lean b/Mathlib/NumberTheory/LSeries/ZMod.lean
@@ -6,7 +6,7 @@ Authors: David Loeffler
 module
 
 public import Mathlib.Analysis.Fourier.ZMod
-public import Mathlib.Analysis.NormedSpace.Connected
+public import Mathlib.Analysis.Normed.Module.Connected
 public import Mathlib.NumberTheory.LSeries.RiemannZeta
 
 /-!
diff --git a/Mathlib/NumberTheory/ModularForms/DedekindEta.lean b/Mathlib/NumberTheory/ModularForms/DedekindEta.lean
@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Analysis.Complex.LocallyUniformLimit
 public import Mathlib.Analysis.Complex.UpperHalfPlane.Exp
-public import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
+public import Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
 
 /-!
 # Dedekind eta function
