mathlib3

16c8f7f3 - feat(algebraic_geometry/prime_spectrum): Basic opens are compact (#7411)

feat(algebraic_geometry/prime_spectrum): Basic opens are compact (#7411) This proves that basic opens are compact in the zariski topology. Compactness of the whole space is then realized as a special case. Also adds a few lemmas about zero loci.