Theorem alg_hom.norm_apply_le_self

refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) …

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