Commit 2024-07-11 01:10 4eb7373b
View on Github →chore (AlgebraicGeometry.PrimeSpectrum): move results not requiring Zariski topology to files in RingTheory (#14631)
Results from AlgebraicGeometry are used back in RingTheory with many unecessary imports coming along with it. We move all possible results from AlgebraicGeometry.PrimeSpectrum.Basic and AlgebraicGeometry.PrimeSpectrum.Noetherian to a new file RingTheory.PrimeSpectrum and all possilbe results from AlgebraicGeometry.PrimeSpectrum.Maximal to a new file RingTheory.MaximalSpectrum.