Galois and Abel-Ruffini theorem 1.2.1

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.12 to 1.15 and Coq from 8.10 to 8.16.

Galois and Abel-Ruffini theorem 1.2.0

This is a full proof Coq/mathcomp of Galois and Abel-Ruffini theorem about the unsolvability of the quintic.
Compared to version 1.1, the proof that a solvable extension is solvable by radicals now uses Hilbert's Theorem 90 instead of matrix diagonalization.
It is compatible with mathcomp version 1.12 and 1.13 and Coq from 8.10 to 8.14.

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.

Galois and Abel-Ruffini theorem 1.0.0

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.