nonempty spectrum of finite dimensional

Stream: general

[Jireh Loreaux]

I've recently been developing the spectrum (in algebra/algebra/spectrum among other places). Recently, I noticed that in field_theory/is_alg_closed/basic (which will be an import of algebra/algebra/spectrum after #10783 merges), there is a proof that every element of a finite dimensional algebra over an algebraically closed field has nonempty spectrum. This is used in two places in mathlib: category_theory/preadditive/schur and linear_algebra/eigenspace. Does anyone object to my moving this theorem into the spectrum file and updating the references accordingly? @Scott Morrison I'm asking you specifically since git blame tells me you added this in its current form.

[Jireh Loreaux]

Note: there is currently some inadvertent code duplication / similarity between exists_spectrum_of_is_alg_closed_of_finite_dimensional in field_theory/is_alg_closed/basic and map_polynomial_of_degree_pos in #10783 which I would also like to clean up.

[Scott Morrison]

Sorry about the delay in replying. Yes, of course it is okay to move this!