Mathlib v3 is deprecated. Go to Mathlib v4

Theorem jordan_holder_lattice.is_maximal_inf_right_of_is_maximal_sup

Modification history

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