Commit 2026-01-24 19:14 e9d4384e

View on Github →

feat(Spectrum/Prime/Topology): Ring.KrullDimLE.eq_bot_or_eq_top (#33607) Given a local ring R which is also a domain with Ring.KrullDimLE 1 R (or equivalently Ring.DimensionLEOne) a prime is either ⊥ or⊤. The application I have in mind is IsDiscreteValuationRing R.

Estimated changes

Modified Mathlib/Order/KrullDimension.lean

modified theorem Order.krullDim_le_one_iff_forall_isMax

modified theorem Order.krullDim_le_one_iff_forall_isMin

added theorem Order.krullDim_le_one_iff_of_boundedOrder

Modified Mathlib/RingTheory/Spectrum/Prime/Topology.lean

added theorem IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top