Quentin VERMANDE
Quentin VERMANDE
Generalizes the definition of radical extension and the Abel-Galois theorem to fields of any characteristic.
##### Motivation for this change Extracts the part from https://github.com/math-comp/math-comp/pull/944 that concern fingroup. Depends on: - https://github.com/math-comp/math-comp/pull/1195 ##### Things done/to do - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` -...
##### Motivation for this change Extracts the parts from https://github.com/math-comp/math-comp/pull/944 that concern `falgebra.v` and `fieldext.v`. Depends on: - https://github.com/math-comp/math-comp/pull/1199 ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md`...
##### Motivation for this change Add algR in `algC.v`, as part of the backport from Abel. N.B. The code comes from Abel/master, not CohenCyril/Abel_backports Depends on: - https://github.com/math-comp/math-comp/pull/1198 ##### Things...
##### Motivation for this change Extracts the part from https://github.com/math-comp/math-comp/pull/944 that concern solvable (with a few things moved to `zmodp`). Depends on: - https://github.com/math-comp/math-comp/pull/1196 ##### Things done/to do - [x]...
##### Motivation for this change Generalizes the operations on ordinals in `zmodp.v` so that `opp`, `add`, `mul` and `inv` are defined on the ordinal `I_0`. ##### Minimal TODO list -...
##### Motivation for this change Changes the name and statement of `eisenstein`, as per the review comments on #1198. ##### Minimal TODO list - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md`...
This PR adds better support for coercions: - declares the constructor of the class as an elpi coercion, using `elaborate-skeleton` to fill in the holes, - declares the `sort` projection...
Some proofs rely on the fact that the proof of membership in I_n comes from inZp, which is not the case anymore with https://github.com/math-comp/math-comp/pull/1229.
##### Motivation for this change Adds the main structures with one operation, i.e. magmas, unitary magmas, semigroups, monoids and groups and refactors N-modules and Z-modules with them. TODO: - [x]...