Mathlib Changelog
v4
Changelog
About
Github
Theorem
Order.krullDim_of_isSimpleOrder
Modification history
2025-03-03 08:08
Mathlib/Order/KrullDimension.lean
feat(Order/KrullDimension): some lemmas relating `Order.height`, `Order.coheight` and `krullDim` (#22236) …
Added
Order.krullDim_of_isSimpleOrder
View on Github →