Abel
Abel copied to clipboard
math-comp
A proof of Abel-Ruffini theorem.
Removes algR, which is backported here: - https://github.com/math-comp/math-comp/pull/1199
The lemmas in various.v for the package algebra have been backported here: - https://github.com/math-comp/math-comp/pull/1198
The lemmas in `various.v` for ssralg and poly have been backported here: - https://github.com/math-comp/math-comp/pull/1185 Relies on https://github.com/math-comp/Abel/pull/85
The lemmas in `various.v` for the package ssreflect have been backported here: - https://github.com/math-comp/math-comp/pull/1193 - https://github.com/math-comp/math-comp/pull/1184
The lemmas in various.v for the package algebra have been backported here : - https://github.com/math-comp/math-comp/pull/1196
The lemmas in various.v for the package algebra have been backported here (modulo https://github.com/math-comp/Abel/pull/86): - https://github.com/math-comp/math-comp/pull/1195
I'm trying to upgrade the Coq packages in Debian using Coq 8.18 and MC2, and this is one of the blockers. Thanks!
Generalizes the definition of radical extension and the Abel-Galois theorem to fields of any characteristic.
