Unsolvability of the Quintic Formalized in Dependent Type Theory - Ecole Centrale de Nantes Accéder directement au contenu
Communication Dans Un Congrès Année : 2021

Unsolvability of the Quintic Formalized in Dependent Type Theory

Résumé

In this paper, we describe an axiom-free Coq formalization that there does not exists a general method for solving by radicals polynomial equations of degree greater than 4. This development includes a proof of Galois’ Theorem of the equivalence between solvable extensions and extensions solvable by radicals. The unsolvability of the general quintic follows from applying this theorem to a well chosen polynomial with unsolvable Galois group.
Fichier principal
Vignette du fichier
main.pdf (750.84 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03136002 , version 1 (09-02-2021)
hal-03136002 , version 2 (20-04-2021)
hal-03136002 , version 3 (21-04-2021)
hal-03136002 , version 4 (02-05-2021)

Identifiants

  • HAL Id : hal-03136002 , version 4

Citer

Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub. Unsolvability of the Quintic Formalized in Dependent Type Theory. ITP 2021 - 12th International Conference on Interactive Theorem Proving, Jun 2021, Rome / Virtual, France. ⟨hal-03136002v4⟩
489 Consultations
659 Téléchargements

Partager

Gmail Facebook X LinkedIn More