Skip to content

Commit 405bba7

Browse files
committed
chore: move Data/Real/StarOrdered to Algebra/Order/Star/Real (leanprover-community#39974)
and update the directory dependency linter accordingly.
1 parent 718a853 commit 405bba7

4 files changed

Lines changed: 5 additions & 3 deletions

File tree

Mathlib.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1104,6 +1104,7 @@ public import Mathlib.Algebra.Order.Star.Basic
11041104
public import Mathlib.Algebra.Order.Star.Conjneg
11051105
public import Mathlib.Algebra.Order.Star.Pi
11061106
public import Mathlib.Algebra.Order.Star.Prod
1107+
public import Mathlib.Algebra.Order.Star.Real
11071108
public import Mathlib.Algebra.Order.Sub.Basic
11081109
public import Mathlib.Algebra.Order.Sub.Defs
11091110
public import Mathlib.Algebra.Order.Sub.Prod
@@ -4287,7 +4288,6 @@ public import Mathlib.Data.Real.Embedding
42874288
public import Mathlib.Data.Real.Pointwise
42884289
public import Mathlib.Data.Real.Sign
42894290
public import Mathlib.Data.Real.Star
4290-
public import Mathlib.Data.Real.StarOrdered
42914291
public import Mathlib.Data.Rel
42924292
public import Mathlib.Data.Rel.Cover
42934293
public import Mathlib.Data.Rel.Separated

Mathlib/Tactic/Linter/DirectoryDependency.lean

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -620,11 +620,13 @@ def overrideAllowedImportDirs : NamePrefixRel := .ofArray #[
620620
(`Mathlib.RepresentationTheory.Continuous, `Mathlib.Topology), -- For continuous representations
621621

622622
-- TODO: reduce these with further moving files out of `Data`
623-
(`Mathlib.Data.Real.StarOrdered, `Mathlib.Analysis),
624623
(`Mathlib.Data.Rat.NatSqrt.Real, `Mathlib.Analysis),
625624
-- TODO: think about the role of Analysis and Algebra, and perhaps further separation
626625
(`Mathlib.Algebra.Order.Archimedean.Real, `Mathlib.Analysis),
627626
(`Mathlib.Algebra.Star.CHSH, `Mathlib.Analysis),
627+
(`Mathlib.Algebra.Order.Star.Real, `Mathlib.Analysis),
628+
(`Mathlib.Topology.ContinuousMap.ContinuousSqrt, `Mathlib.Algebra.Order),
629+
(`Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus, `Mathlib.Algebra.Order),
628630
(`Mathlib.Algebra.Order.Ring.StandardPart, `Mathlib.Analysis),
629631
]
630632

Mathlib/Topology/ContinuousMap/ContinuousSqrt.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@ Authors: Jireh Loreaux
55
-/
66
module
77

8+
public import Mathlib.Algebra.Order.Star.Real
89
public import Mathlib.Analysis.Complex.Basic
9-
public import Mathlib.Data.Real.StarOrdered
1010
public import Mathlib.Topology.ContinuousMap.StarOrdered
1111

1212
/-! # Instances of `ContinuousSqrt`

0 commit comments

Comments
 (0)