Theorem IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top

Modification history

2026-01-24 19:14

Mathlib/RingTheory/Spectrum/Prime/Topology.lean

feat(Spectrum/Prime/Topology): Ring.KrullDimLE.eq_bot_or_eq_top (#33607) …

Added IsLocalRing.Ring.KrullDimLE.eq_bot_or_eq_top View on Github →