Commit 2025-01-10 18:07 d9e6deb2

refactor: remove the CompactSpace field from Unique{NonUnital}ContinuousFunctionalCalculus (#20590) This was originally useful for the general theory in some places, but since that time, this field is included in ContinuousFunctionalCalculus itself. This PR removes this fields, which means that any topological 𝕜-algebra is an instance of this class. (for RCLike 𝕜). Moreover, a topological 𝕜-algebra A also has a UniqueContinuousFunctionalCalculus ℝ≥0 A instance. Previously, we only had this for normed 𝕜-algebras because of the compact spectrum criterion. This avoids the need to assume [UniqueContinuousFunctionalCalculus 𝕜 A] pretty much throughout the library, replacing it with [T2Space A] and, in the case of 𝕜 := ℝ≥0, [TopologicalRing A].