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 -

Fuente: https://hal.archives-ouvertes.fr/



DESCARGAR PDF




Documentos relacionados