Theorem Order.krullDim_le_one_iff_forall_isMax

Modification history

2026-01-24 19:14
Mathlib/Order/KrullDimension.lean
feat(Spectrum/Prime/Topology): Ring.KrullDimLE.eq_bot_or_eq_top (#33607) …
Modified Order.krullDim_le_one_iff_forall_isMaxView on Github →
2024-12-29 20:14
Mathlib/Order/KrullDimension.lean
feat(Order/KrullDimension): equivalent conditions for zero-dimensional, one-dimensional etc (#20176)
Added Order.krullDim_le_one_iff_forall_isMaxView on Github →