Commit 2025-04-14 15:20 c9486a6f
View on Github →feat(RingTheory/LocalRing): IsLocalRing.of_singleton_maximalSpectrum (#23994)
Add the fact that a ring with MaximalSpectrum that is a singleton is local.
feat(RingTheory/LocalRing): IsLocalRing.of_singleton_maximalSpectrum (#23994)
Add the fact that a ring with MaximalSpectrum that is a singleton is local.