A Modular Formalisation of Finite Group Theory

  • Georges Gonthier ,
  • Assia Mahboubi ,
  • Laurence Rideau ,
  • Enrico Tassi ,
  • Laurent Théry

Published by Springer-Verlag

Télécharger BibTex

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.