mathlib3

d7c689d2 - feat(algebraic_geometry/prime_spectrum): Closed points in prime spectrum (#9861)

feat(algebraic_geometry/prime_spectrum): Closed points in prime spectrum (#9861) This PR adds lemmas about the correspondence between closed points in `prime_spectrum R` and maximal ideals of `R`. In order to import and talk about integral maps I had to move some lemmas from `noetherian.lean` to `prime_spectrum.lean` to prevent cyclic import dependencies.