Theorem RCLike.uniqueNonUnitalContinuousFunctionalCalculus_of_compactSpace_quasispectrum

Modification history

2025-01-10 18:07
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
refactor: remove the `CompactSpace` field from `Unique{NonUnital}ContinuousFunctionalCalculus` (#20590) …
Deleted RCLike.uniqueNonUnitalContinuousFunctionalCalculus_of_compactSpace_quasispectrumView on Github →
2024-06-02 02:44
Mathlib/Topology/ContinuousFunction/UniqueCFC.lean
feat: uniqueness of the non-unital continuous functional calculus (#13363)
Added RCLike.uniqueNonUnitalContinuousFunctionalCalculus_of_compactSpace_quasispectrumView on Github →