mathlib3

e944a998 - feat(algebraic_geometry/projective_spectrum) : lemmas about `vanishing_ideal` and `zero_locus` (#12730)

feat(algebraic_geometry/projective_spectrum) : lemmas about `vanishing_ideal` and `zero_locus` (#12730) This pr mimics the corresponding construction in `Spec`; other than `projective_spectrum.basic_open_eq_union_of_projection` everything else is a direct copy.