Theorem Order.coheight_coe_withTop

Modification history

2026-09-04 09:44
Mathlib/Order/KrullDimension.lean
chore(Order/WithBot): remove defeq between `WithBot.LE`/`LT` and `WithTop.LE`/`LT` (#42622) …
Modified Order.coheight_coe_withTopView on Github →
2024-11-20 12:32
Mathlib/Order/KrullDimension.lean
feat(KrullDimension): concrete calculations (#19210) …
Added Order.coheight_coe_withTopView on Github →