mathlib3

a8bfcfed - feat(algebraic_geometry/projective_spectrum): basic definitions of projective spectrum (#12635)

feat(algebraic_geometry/projective_spectrum): basic definitions of projective spectrum (#12635) This pr contains the basic definitions of projective spectrum of a graded ring: - projective spectrum - zero locus - vanishing ideal