Commit 2025-03-03 08:08 4b6faf03

View on Github →

feat(Order/KrullDimension): some lemmas relating Order.height, Order.coheight and krullDim (#22236) This PR mostly consists of the lemmas related to Order.height, Order.coheight, and krullDim appearing in the process of working on PR #21041. We thought that the lemmas may be useful to other PRs (like #22127 perhaps?), so we decided to open it into a separate PR to accelerate the review process.

Estimated changes

Modified Mathlib/Order/KrullDimension.lean

added theorem Order.coheight_eq_krullDim_Ici

added theorem Order.finiteDimensionalOrder_iff_krullDim_ne_bot_and_top

added theorem Order.height_eq_krullDim_Iic

added theorem Order.krullDim_of_isSimpleOrder

Modified Mathlib/Order/RelSeries.lean

added theorem LTSeries.nonempty_of_finiteDimensionalOrder

added theorem LTSeries.nonempty_of_infiniteDimensionalOrder

deleted theorem LTSeries.nonempty_of_infiniteDimensionalType

added theorem RelSeries.nonempty_of_finiteDimensional