A Modular Formalisation of Finite Group Theory

Abstract : 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 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.
Liste complète des métadonnées

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/inria-00139131
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, April 3, 2007 - 11:48:23 AM
Last modification on : Saturday, September 17, 2016 - 1:36:42 AM
Document(s) archivé(s) le : Tuesday, September 21, 2010 - 12:47:34 PM

Files

RR-6156.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00139131, version 2

Collections

Citation

Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry. A Modular Formalisation of Finite Group Theory. [Research Report] RR-6156, INRIA. 2007, pp.17. 〈inria-00139131v2〉

Share

Metrics

Record views

914

Document downloads

397