Theorem Order.krullDim_nonpos_iff_forall_isMin

Modification history

2024-12-29 20:14

Mathlib/Order/KrullDimension.lean

feat(Order/KrullDimension): equivalent conditions for zero-dimensional, one-dimensional etc (#20176)

Added Order.krullDim_nonpos_iff_forall_isMin View on Github →