Mathlib v3 is deprecated. Go to Mathlib v4

Theorem composition_series.lt_succ

Modification history

2021-10-04 09:48

src/order/jordan_holder.lean

feat(order/jordan_holder): Jordan Hölder theorem (#8976) …

Added composition_series.lt_succ View on Github →