The Jordan-Hölder Theorem

Title:	The Jordan-Hölder Theorem
Author:	Jakob von Raumer (psxjv4 /at/ nottingham /dot/ ac /dot/ uk)
Submission date:	2014-09-09
Abstract:	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.
BibTeX:	@article{Jordan_Hoelder-AFP, author = {Jakob von Raumer}, title = {The Jordan-Hölder Theorem}, journal = {Archive of Formal Proofs}, month = sep, year = 2014, note = {\url{http://isa-afp.org/entries/Jordan_Hoelder.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Secondary_Sylow
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.