Commit 2024-11-04 20:06 ba252b3c

View on Github →

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

Estimated changes

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Jacobson.lean

modified theorem PrimeSpectrum.exists_isClosed_singleton_of_isJacobsonRing

added theorem PrimeSpectrum.isJacobsonRing_iff_jacobsonSpace

Modified Mathlib/RingTheory/Jacobson.lean

Modified Mathlib/RingTheory/JacobsonIdeal.lean

added theorem Ideal.isRadical_jacobson

Modified Mathlib/Topology/JacobsonSpace.lean

modified theorem closedPoints_eq_univ