mathlib

689184f7 - feat(algebraic_geometry/prime_spectrum/noetherian): The spectrum of a noetherian ring is noetherian. (#17016)

feat(algebraic_geometry/prime_spectrum/noetherian): The spectrum of a noetherian ring is noetherian. (#17016) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>