mathlib3
58a27226 - chore(algebra/algebra/spectrum): split file (#19161)

Commit
2 years ago
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`.
Author
Parents
Loading