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.
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.