Mathlib v3 is deprecated. Go to Mathlib v4

Theorem composition_series.eq_of_bot_eq_bot_of_top_eq_top_of_length_eq_zero

Modification history

2021-10-04 09:48
src/order/jordan_holder.lean
feat(order/jordan_holder): Jordan Hölder theorem (#8976) …
Added composition_series.eq_of_bot_eq_bot_of_top_eq_top_of_length_eq_zeroView on Github →