Theorem Order.krullDim_eq_one_iff_of_boundedOrder

Modification history

2025-04-04 14:05
Mathlib/Order/KrullDimension.lean
feat(RingTheory): lengths of modules (#23663)
Added Order.krullDim_eq_one_iff_of_boundedOrderView on Github →