Commit 2024-10-28 14:43 41221c61

View on Github →

feat(AlgebraicGeometry/PrimeSpectrum): prime spectrum of jacobson rings (#18242)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

added theorem PrimeSpectrum.isMax_iff

added theorem PrimeSpectrum.isMin_iff

added theorem PrimeSpectrum.stableUnderGeneralization_singleton

added theorem PrimeSpectrum.stableUnderSpecialization_singleton

added theorem PrimeSpectrum.zeroLocus_eq_iff

Created Mathlib/AlgebraicGeometry/PrimeSpectrum/Jacobson.lean

added theorem PrimeSpectrum.exists_isClosed_singleton_of_isJacobson

added theorem PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobson

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Noetherian.lean

added theorem PrimeSpectrum.finite_setOf_isMin