Theorem Order.coheight_coe_withBot

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_withBot View on Github →

2024-11-20 12:32

Mathlib/Order/KrullDimension.lean

feat(KrullDimension): concrete calculations (#19210) …

Added Order.coheight_coe_withBot View on Github →