Theorem LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot

Modification history

2025-04-04 14:05
Mathlib/Order/RelSeries.lean
feat(RingTheory): lengths of modules (#23663)
Added LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_botView on Github →