Theorem spectrum.nonempty

feat(analysis/normed_space/spectrum): lemmas about spectral radius, spectral mapping and `alg_hom_class` maps into the base field (#17178) …

feat(algebra/algebra/spectrum, analysis/normed_space/spectrum): prove the spectrum of any element in a complex Banach algebra is nonempty (#12115) …