Def CStarAlgebra.spectralOrder

Modification history

2025-01-14 02:38

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean

refactor: split `Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances` in a principled way (#20647) …

Modified CStarAlgebra.spectralOrder View on Github →

2024-09-12 16:24

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

chore: namespace lemmas to `CStarAlgebra` instead of `CStarRing` (#16653) …

Added CStarAlgebra.spectralOrder View on Github →