Commit 2020-02-22 20:47 ea149c8d
View on Github →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