Theorem LTSeries.nonempty_of_infiniteDimensionalType

Modification history

2025-03-03 08:08

Mathlib/Order/RelSeries.lean

feat(Order/KrullDimension): some lemmas relating `Order.height`, `Order.coheight` and `krullDim` (#22236) …

Deleted LTSeries.nonempty_of_infiniteDimensionalType View on Github →

2023-09-18 04:21

Mathlib/Order/RelSeries.lean

feat: rework `StrictSeries` to `RelSeries` (#7221) …

Added LTSeries.nonempty_of_infiniteDimensionalType View on Github →