In this paper, we present a formalisation of elementary group theory done in COQ. This work is the first milestone of a long-term effort to formalise the Feit-Thompson theorem. As our further developments will heavily rely on this initial base, we took special care to articulate it in the most compositional way. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., & Théry, L. (2007). A modular formalisation of finite group theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4732 LNCS, pp. 86–101). Springer Verlag. https://doi.org/10.1007/978-3-540-74591-4_8
Mendeley helps you to discover research relevant for your work.