mathlib3
71a08c30 - refactor(analysis/normed_space/spectrum): remove `norm_one_class` hypotheses (#16891)

Commit
3 years ago
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`).
Author
Parents
Loading