A Modular Formalisation of Finite Group Theory
- Georges Gonthier ,
- Assia Mahboubi ,
- Laurence Rideau ,
- Enrico Tassi ,
- Laurent Théry
Published by Springer-Verlag
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.