chore: move Analysis/Matrix to Analysis/Matrix/Normed (leanprover-community#31228)

themathqueen · themathqueen · commit 593e3fdf8805 · 2025-11-03T18:58:09.000Z
Since we already have a folder for `Analysis/Matrix`, we should probably move this there. It looks strange on the documentation otherwise.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1780,7 +1780,7 @@ import Mathlib.Analysis.LocallyConvex.WeakDual
 import Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
 import Mathlib.Analysis.LocallyConvex.WeakSpace
 import Mathlib.Analysis.LocallyConvex.WithSeminorms
-import Mathlib.Analysis.Matrix
+import Mathlib.Analysis.Matrix.Normed
 import Mathlib.Analysis.Matrix.Order
 import Mathlib.Analysis.MeanInequalities
 import Mathlib.Analysis.MeanInequalitiesPow
diff --git a/Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean b/Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
@@ -5,7 +5,7 @@ Authors: Frédéric Dupuis
 -/
 
 import Mathlib.Analysis.CStarAlgebra.Module.Constructions
-import Mathlib.Analysis.Matrix
+import Mathlib.Analysis.Matrix.Normed
 import Mathlib.Topology.UniformSpace.Matrix
 
 /-!
diff --git a/Mathlib/Analysis/CStarAlgebra/Matrix.lean b/Mathlib/Analysis/CStarAlgebra/Matrix.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Hans Parshall
 -/
 import Mathlib.Analysis.InnerProductSpace.Adjoint
-import Mathlib.Analysis.Matrix
+import Mathlib.Analysis.Matrix.Normed
 import Mathlib.Analysis.RCLike.Basic
 import Mathlib.LinearAlgebra.UnitaryGroup
 import Mathlib.Topology.UniformSpace.Matrix
diff --git a/Mathlib/Analysis/Matrix/Normed.lean b/Mathlib/Analysis/Matrix/Normed.lean
diff --git a/Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean b/Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.Analysis.Normed.Algebra.Exponential
-import Mathlib.Analysis.Matrix
+import Mathlib.Analysis.Matrix.Normed
 import Mathlib.LinearAlgebra.Matrix.ZPow
 import Mathlib.LinearAlgebra.Matrix.Hermitian
 import Mathlib.LinearAlgebra.Matrix.Symmetric
diff --git a/Mathlib/NumberTheory/SiegelsLemma.lean b/Mathlib/NumberTheory/SiegelsLemma.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Fabrizio Barroero. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Barroero, Laura Capuano, Amos Turchet
 -/
-import Mathlib.Analysis.Matrix
+import Mathlib.Analysis.Matrix.Normed
 import Mathlib.Data.Pi.Interval
 import Mathlib.Tactic.Rify
 
