chore: deprecate Analysis/Normed/Order/Basic (leanprover-community#34047)

grunweg · grunweg · commit 7ee74e7d3f87 · 2026-01-16T21:39:34.000Z
It is empty.
diff --git a/Mathlib/Analysis/Normed/Order/Basic.lean b/Mathlib/Analysis/Normed/Order/Basic.lean
@@ -13,3 +13,5 @@ public import Mathlib.Analysis.Normed.Group.Basic
 In this file, we define classes for fields and groups that are both normed and ordered.
 These are mostly useful to avoid diamonds during type class inference.
 -/
+
+deprecated_module (since := "2026-01-16")
