Formalising Sylows theorems in CoqReportar como inadecuado

Formalising Sylows theorems in Coq - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

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.

Keywords : Group theory Sylow-s theorems Formalisation of mathematics

Autor: Laurent Thery - Laurence Rideau -



Documentos relacionados