mathlib3

ea149c8d - feat(algebraic_geometry/prime_spectrum): prime spectrum of a ring is compact (#1987)

feat(algebraic_geometry/prime_spectrum): prime spectrum of a ring is compact (#1987) * wip * wip * wip * wip * WIP * WIP * Reset changes that belong to other PR * Docstrings * Add Heine--Borel to docstring * Cantor's intersection theorem * Cantor for sequences * Revert "Reset changes that belong to other PR" This reverts commit e6026b8819570ef6a763582a25d7ae5ad508134b. * Move submodule lemmas to other file * Fix build * Update prime_spectrum.lean * Docstring * Update prime_spectrum.lean * Slight improvement? * Slightly improve structure of proof * WIP * Cleaning up proofs * Final fixes Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>