Galois and Abel-Ruffini theorem 1.1.2
This is a full proof Coq/mathcomp of Galois and Abel-Ruffini theorem about the unsolvability of the quintic.
It is compatible with mathcomp version 1.11 and 1.12 and Coq from 8.10 to 8.13.
This is the company material for the ITP 2021 paper.