Commit 2022-10-10 20:56 71a08c30

refactor(analysis/normed_space/spectrum): remove norm_one_class hypotheses (#16891) When this file and its main results were created, mathlib had a different definition of normed_algebra which automatically entailed norm_one_class. When normed_algebra was refactored, this hypothesis was added everywhere it was needed, including this file. However, most of the main results here are independent of that assumption, but the proof requires slightly more work. Here, we do that work so that we can remove these hypotheses here and a few places downstream. For a few results, we provide both the norm_one_class version, and the version without it for convenience (especially because any nontrivial cstar_ring automatically satisfies norm_one_class).