Skip to content

Galois and Abel-Ruffini theorem 1.2.0
Compare
Choose a tag to compare
@CohenCyril CohenCyril released this 28 Oct 22:51
· 31 commits to master since this release
1.2.0
3a7b4fe
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Learn about vigilant mode.

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.

Assets 2