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.