inria-00113750, version 2
Formalising Sylow's theorems in Coq
Laurent Thery
1Laurence Rideau 1
N° RT-0327 (2006)
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.
- 1: MARELLE (INRIA Sophia Antipolis)
- INRIA
- Domain : Computer Science/Logic in Computer Science
- Keywords : Group theory – Sylow's theorems – Formalisation of mathematics
- Internal note : RT-0327
- Available versions : v1 (2006-11-14) v2 (2006-11-22)
- inria-00113750, version 2
- http://hal.inria.fr/inria-00113750
- oai:hal.inria.fr:inria-00113750
- From: Rapport De Recherche Inria
- Submitted on: Wednesday, 22 November 2006 13:29:33
- Updated on: Wednesday, 1 October 2008 11:07:08
Associated documents
Export