Commit 2021-11-30 07:29 4a9aa275

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.