Abstract
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.
Language: English
Page range: 35 - 51
Published on: Jun 9, 2008
Published by: University of Białystok
In partnership with: Paradigm Publishing Services
Publication frequency: 1 issue per year
Related subjects:
© 2008 Marco Riccardi, published by University of Białystok
This work is licensed under the Creative Commons License.