Secondary Sylow swMATH ID: 29536 Software Authors: Jakob von Raumer Description: 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. Homepage: https://www.isa-afp.org/entries/Secondary_Sylow.html Dependencies: Isabelle Related Software: Archive Formal Proofs; Automath; Locales; Isabelle; Jordan Hölder; Isabelle/HOL; Jacobson_Basic_Algebra; Coq; IMPS; PVS; LARCH Cited in: 2 Publications Cited by 3 Authors 1 Ballarin, Clemens 1 Kammüller, Florian 1 Paulson, Lawrence Charles Cited in 1 Serial 2 Journal of Automated Reasoning Cited in 3 Fields 2 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) 1 Group theory and generalizations (20-XX) Citations by Year