# [isabelle] New AFP entry: The Jordan-Hölder Theorem

*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] New AFP entry: The Jordan-Hölder Theorem
*From*: Tobias Nipkow <nipkow at in.tum.de>
*Date*: Thu, 11 Sep 2014 11:00:31 +0200
*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:24.0) Gecko/20100101 Thunderbird/24.6.0

The Jordan-Hölder Theorem
Jakob von Raumer
This submission contains theories that lead to a formalization of the proof of
the Jordan-Hölder theorem about composition series of finite groups. The
theories formalize the notions of isomorphism classes of groups, simple groups,
normal series, composition series, maximal normal subgroups. Furthermore, they
provide proofs of the second isomorphism theorem for groups, the
characterization theorem for maximal normal subgroups as well as many useful
lemmas about normal subgroups and factor groups. The proof is inspired by course
notes of Stuart Rankin.
http://afp.sourceforge.net/entries/Jordan_Hoelder.shtml
Enjoy!

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*