Theorem PrimeSpectrum.exists_isClosed_singleton_of_isJacobsonRing

Modification history

2024-11-04 20:06

Mathlib/AlgebraicGeometry/PrimeSpectrum/Jacobson.lean

feat(AlgebraicGeometry): prime spectrum of jacobson rings are jacobson spaces (#18353)

Modified PrimeSpectrum.exists_isClosed_singleton_of_isJacobsonRing View on Github →

2024-10-31 23:26

Mathlib/AlgebraicGeometry/PrimeSpectrum/Jacobson.lean

chore(RingTheory/Jacobson): Rename `Ideal.IsJacobson` to `IsJacobsonRing`. (#18271)

Added PrimeSpectrum.exists_isClosed_singleton_of_isJacobsonRing View on Github →