Theorem Order.krullDim_eq_top_of_infiniteDimensionalOrder

Modification history

2024-12-29 20:14

Mathlib/Order/KrullDimension.lean

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

Deleted Order.krullDim_eq_top_of_infiniteDimensionalOrder View on Github →

2024-09-05 10:13

Mathlib/Order/KrullDimension.lean

feat(KrullDimension): height refactor, initial stuff (#16480) …

Added Order.krullDim_eq_top_of_infiniteDimensionalOrder View on Github →