À propos de cet article
Publié en ligne: 09 juin 2008
Pages: 35 - 51
DOI: https://doi.org/10.2478/v10037-007-0005-8
This content is open access.
The goal of this article is to formalize the Jordan-Hölder theorem in the context of group with operators as in the book [5]. Accordingly, the article introduces the structure of group with operators and reformulates some theorems on a group already present in the Mizar Mathematical Library. Next, the article formalizes the Zassenhaus butterfly lemma and the Schreier refinement theorem, and defines the composition series.