Commit 2024-04-07 23:15 67a73e5a

feat: add a class to encode that the spectrum of nonnegative elements is nonnegative (#11993) When working with the continuous functional calculus generically, it is currently hard to establish lemmas that work well for positive across the board. This is in part due to the fact that one cannot conclude from the continuous functional calculus alone that the spectrum of nonnegative elements in a star-ordered ring is nonnegative. So, we use a type class to encode this, and this type class actually uses the quasispectrum, because for unital algebras the two notions are equivalent.