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.