Jordan Hölder

swMATH ID: 29552
Software Authors: Jakob von Raumer
Description: Archive of formal proofs: The Jordan-Hölder Theorem. 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.
Homepage: https://www.isa-afp.org/entries/Jordan_Hoelder.html
Keywords: Archive of formal proofs; Jordan-Hölder Theorem; Isabelle/HOL; proof; Groups; composition series; subgroups
Related Software: Archive Formal Proofs; Secondary Sylow
Cited in: 0 Publications

Standard Articles

1 Publication describing the Software Year