Commit 2023-06-06 17:18 58a27226

chore(algebra/algebra/spectrum): split file (#19161) This splits off all the material related to polynomials from algebra.algebra.spectrum into a new file field_theory.is_alg_closed.spectrum, because (almost) all of it requires is_alg_closed 𝕜. This significantly simplifies the import tree for this file, and for a few files which import it. This also does two minor housekeeping chores:

1. generalizes type class assumptions for alg_hom.mem_resolvent_set_apply and alg_hom.spectrum_apply_subset
2. rephrases spectrum.nonempty_of_is_alg_closed_of_finite_dimensional to use set.nonempty.