Commit 2024-11-15 17:12 1fb5d8c3

View on Github →

feat(KrullDimension): height and 0, ⊤, ⊥, coe (#19028) Next parts from PR #15524: relating height to 0, ⊤, ⊥, coe. From the Carleson project

Estimated changes

Modified Mathlib/Order/KrullDimension.lean

added theorem Order.coe_lt_height_iff

added theorem Order.height_bot

added theorem Order.height_eq_coe_add_one_iff

added theorem Order.height_eq_coe_iff

modified theorem Order.height_eq_iSup_lt_height

added theorem Order.height_eq_top_iff

added theorem Order.height_eq_zero

modified theorem Order.height_le_coe_iff