mathlib

4a9aa275 - feat(analysis/normed_space/spectrum and algebra/algebra/spectrum): prove properties of spectrum in a Banach algebra (#10530)

feat(analysis/normed_space/spectrum and algebra/algebra/spectrum): prove properties of spectrum in a Banach algebra (#10530) Prove that the `spectrum` of an element in a Banach algebra is closed and bounded, hence compact when the scalar field is proper. Compute the derivative of the `resolvent a` function in preparation for showing that the spectrum is nonempty when the base field is ℂ. Define the `spectral_radius` and prove that it is bounded by the norm. Also rename the resolvent set to `resolvent_set` instead of `resolvent` so that it doesn't clash with the function name.