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

theorem Ideal.finite_minimalPrimes_of_isNoetherianRing (R : Type u) [CommRing R] [IsNoetherianRing R] (I : Ideal R) : I.minimalPrimes.Finite

instance PrimeSpectrum.instKrullDimLEOfNatNat (R : Type u) [CommRing R] [IsArtinianRing R] : Ring.KrullDimLE 0 R

instance PrimeSpectrum.instDiscreteTopology (R : Type u) [CommRing R] [IsArtinianRing R] : DiscreteTopology (PrimeSpectrum R)

theorem IsArtinianRing.exists_not_mem_forall_mem_of_ne {R : Type u} [CommRing R] [IsArtinianRing R] (p : Ideal R) [p.IsPrime] : ∃ r ∉ p, IsIdempotentElem r ∧ ∀ (q : Ideal R), q.IsPrime → q ≠ p → r ∈ q