search

leanprover-community / mathlib

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k stars 297 forks source link

[Merged by Bors] - chore(algebra/algebra/spectrum): split file #19161

Closed j-loreaux closed 1 year ago

j-loreaux commented 1 year ago

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.

Although this is just a useful split, it will also open up some new files for porting.

Open in Gitpod

urkud commented 1 year ago

Thanks! Once CI is happy, please merge this PR using bors r+ bors d+

bors[bot] commented 1 year ago

:v: j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

j-loreaux commented 1 year ago

bors r+

bors[bot] commented 1 year ago

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here. For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.