mathlib3

9bdc5551 - feat(algebraic_geometry/prime_spectrum): More lemmas (#7244)

feat(algebraic_geometry/prime_spectrum): More lemmas (#7244) Adding and refactoring some lemmas about zero loci and basic opens. Also adds three lemmas in `ideal/basic.lean`.