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.
Type de document :
Rapport
[Technical Report] RT-0327, INRIA. 2006, pp.23
Liste complète des métadonnées

https://hal.inria.fr/inria-00113750
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 22 novembre 2006 - 13:29:33
Dernière modification le : jeudi 11 janvier 2018 - 16:41:59
Document(s) archivé(s) le : lundi 20 septembre 2010 - 17:21:41

Fichiers

RT-0327.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

417

Téléchargements de fichiers

166