Commit 2022-03-06 15:06 0a6efe0f
View on Github →feat(analysis/normed_space/star/spectrum): prove the spectral radius of a star normal element is its norm (#12249) In a C⋆-algebra over ℂ, the spectral radius of any star normal element is its norm. This extends the corresponding result for selfadjoint elements.