Commit 2021-10-27 15:13 d7c689d2

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.