Theorem Order.krullDim_le_one_iff_of_boundedOrder

Modification history

2026-01-24 19:14
Mathlib/Order/KrullDimension.lean
feat(Spectrum/Prime/Topology): Ring.KrullDimLE.eq_bot_or_eq_top (#33607) …
Added Order.krullDim_le_one_iff_of_boundedOrderView on Github →