chore(Analysis.{CStarAlgebra.ContinuousFunctionalCalculus → Continuou…

…sFunctionalCalculus.SpecialFunctions}): move file `PosPart` (#18930) We have moved this file because it does not import `Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances`, and thereby is more appropriate for the folder dealing with generically usable CFC functions.
leanprover-community · Nov 21, 2024 · 5ba4267 · 5ba4267
1 parent b1faa23
commit 5ba4267
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1040,7 +1040,6 @@ import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
-import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.PosPart
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
@@ -1427,6 +1426,7 @@ import Mathlib.Analysis.SpecialFunctions.Complex.Log
 import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
 import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
 import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog
+import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart
 import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow
 import Mathlib.Analysis.SpecialFunctions.Exp
 import Mathlib.Analysis.SpecialFunctions.ExpDeriv

diff --git a/...ContinuousFunctionalCalculus/PosPart.lean → ...ContinuousFunctionalCalculus/PosPart.lean b/...ContinuousFunctionalCalculus/PosPart.lean → ...ContinuousFunctionalCalculus/PosPart.lean