Commit 2024-04-08 11:30 6212c09c

View on Github →

refactor: generalize instances of the continuous functional calculus (#11944) This refactors instances of the continuous functional calculus slightly. In particular, the derived instances for IsSelfAdjoint and 0 ≤ · will now trigger automatically once the type class conditions are satisfied, and these are generic, not specific to C⋆-algebras. For nonnegative elements, this utilizes the new type class NonnegSpectrumClass. In addition, we show that the restricted continuous functional calculi are equal to their non-restricted counterparts.

Estimated changes