mathlib
8a05dca7 - feat(order/jordan_holder): Jordan Hölder theorem (#8976)

Commit
4 years ago
feat(order/jordan_holder): Jordan Hölder theorem (#8976) The Jordan Hoelder theorem proved for a Jordan Hölder lattice, instances of which include submodules of a module and subgroups of a group. Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
Author
Parents
Loading