Commit 2024-11-20 12:32 cd4d2185

View on Github →

feat(KrullDimension): concrete calculations (#19210) Part of https://github.com/leanprover-community/mathlib4/pull/15524. This adds concrete calculations of the height and Krull Dimension for Nat, Int, WithTop, WithBot and ENat. From the Carleson project.

Estimated changes

Modified Mathlib/Order/KrullDimension.lean

added theorem Order.coheight_coe_enat

added theorem Order.coheight_coe_withBot

added theorem Order.coheight_coe_withTop

added theorem Order.coheight_int

added theorem Order.coheight_nat

added theorem Order.coheight_of_noMaxOrder

added theorem Order.height_coe_withBot

added theorem Order.height_coe_withTop

added theorem Order.height_enat

added theorem Order.height_int

added theorem Order.height_nat

added theorem Order.height_of_noMinOrder

added theorem Order.krullDim_WithTop

added theorem Order.krullDim_enat

added theorem Order.krullDim_int

added theorem Order.krullDim_nat

added theorem Order.krullDim_of_noMaxOrder

added theorem Order.krullDim_of_noMinOrder

added theorem Order.krullDim_withBot