mathlib

5405d294 - refactor(algebraic_geometry/projective_spectrum/topology): refactor projective_spectrum def into structure (#16931)

refactor(algebraic_geometry/projective_spectrum/topology): refactor projective_spectrum def into structure (#16931) - [x] depends on: #16920 [refactor height one spectrum] - [x] depends on: #16930 [refactor prime spectrum]