Commit 2025-02-16 04:57 282ec35e

refactor: use CFC.posPart in a key lemma for C⋆-algebras (#20935) A key lemma for C⋆-algebras says that the spectrum of an element of the form star x * x is nonnegative. The proof uses the continuous functional calculus in an essential way, especially the decomposition into positive and negative parts. Previously, this was done in an ad hoc manner because the general theory of CFC.posPart was undeveloped. We refactor the proof of this lemma to make use of the API, considerably shortening the proof, while we also provide some documentation in the form of comments. Along the way, we extract a few lemmas about the (quasi)spectrum of products of elements, one of which was in the previous version of the lemma mentioned above.