mathlib3

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

feat(algebra/algebra/spectrum, analysis/normed_space/spectrum): prove the spectrum of any element in a complex Banach algebra is nonempty (#12115) This establishes that the spectrum of any element in a (nontrivial) complex Banach algebra is nonempty. The nontrivial assumption is necessary, as otherwise the only element is invertible. In addition, we establish some properties of the resolvent function; in particular, it tends to zero at infinity. - [x] depends on: #12095 Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>