This file proves additional properties of the prime spectrum a ring is Noetherian.

instance PrimeSpectrum.instNoetherianSpace (R : Type u) [CommRing R] [IsNoetherianRing R] : TopologicalSpace.NoetherianSpace (PrimeSpectrum R)

theorem minimalPrimes.finite_of_isNoetherianRing (R : Type u) [CommRing R] [IsNoetherianRing R] : (minimalPrimes R).Finite

theorem PrimeSpectrum.finite_setOf_isMin (R : Type u) [CommRing R] [IsNoetherianRing R] : {x : PrimeSpectrum R | IsMin x}.Finite