mathlib

0a6efe0f - feat(analysis/normed_space/star/spectrum): prove the spectral radius of a star normal element is its norm (#12249)

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. - [x] depends on: #12211 - [x] depends on: #11991