Theorem LTSeries.nonempty_of_infiniteDimensionalOrder

Modification history

2025-03-03 08:08
Mathlib/Order/RelSeries.lean
feat(Order/KrullDimension): some lemmas relating `Order.height`, `Order.coheight` and `krullDim` (#22236) …
Added LTSeries.nonempty_of_infiniteDimensionalOrderView on Github →