chore: deprecate_module for Analysis/Matrix (leanprover-community#31229)

themathqueen · themathqueen · commit f63c76ff5eb8 · 2025-11-03T20:48:35.000Z
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1780,6 +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
diff --git a/Mathlib/Analysis/Matrix.lean b/Mathlib/Analysis/Matrix.lean
@@ -0,0 +1,3 @@
+import Mathlib.Analysis.Matrix.Normed
+
+deprecated_module (since := "2025-11-03")

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+import Mathlib.Analysis.Matrix.Normed`
	`2`	`+`
	`3`	`+deprecated_module (since := "2025-11-03")`