Archive of formal proofs: Secondary Sylow Theorems. These theories extend the existing proof of the first Sylow theorem (written by Florian Kammueller and L. C. Paulson) by what are often called the second, third and fourth Sylow theorems. These theorems state propositions about the number of Sylow p-subgroups of a group and the fact that they are conjugate to each other. The proofs make use of an implementation of group actions and their properties.
Keywords for this software
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Ballarin, Clemens: Exploring the structure of an algebra text with locales (2020)
- Jakob von Raumer: The Jordan-Hölder Theorem (2014) not zbMATH
- Kammüller, Florian; Paulson, Lawrence C.: A formal proof of Sylow’s theorem. An experiment in abstract algebra with Isabelle H0L (1999)