Commit 2024-09-07 09:03 0c583449
View on Github →feat(KrullDimension): Order.height_eq_index_of_length_eq_height_last (#16500)
This pulls the next interesting lemma off the too-large PR #15524, and towards that
creates useful height_le and length_le_height lemmas to show inequalities involving height.
From the Carleson project.