Formalising Sylow's theorems in Coq

Laurent Thery 1 Laurence Rideau 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This report presents a formalisation of Sylow's theorems done in Coq. The formalisation has been done in a couple of weeks on top of Georges Gonthier's ssreflect. There were two ideas behind formalising Sylow's theorems. The first one was to get familiar with Georges way of doing proofs. The second one was to contribute to the collective effort to formalise a large subset of group theory in Coq with some non-trivial proofs.
Document type :
Reports
[Technical Report] RT-0327, INRIA. 2006, pp.23
Liste complète des métadonnées

https://hal.inria.fr/inria-00113750
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, November 22, 2006 - 1:29:33 PM
Last modification on : Saturday, September 17, 2016 - 1:36:46 AM
Document(s) archivé(s) le : Monday, September 20, 2010 - 5:21:41 PM

Files

RT-0327.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Laurent Thery, Laurence Rideau. Formalising Sylow's theorems in Coq. [Technical Report] RT-0327, INRIA. 2006, pp.23. <inria-00113750v2>

Share

Metrics

Record views

291

Document downloads

131