Quentin VERMANDE
Quentin VERMANDE
@CohenCyril I did most of what we discussed, but not right away due to other obligations. Hopefully I did not forget anything. I have issues with generalizing cycle_imset, I added...
@CohenCyril Thank you, I moved the results in temp to their (hopefully) right location in various.v, I also had to move some of the results in map_gal.v there because of...
Thank you for the contribution. I did a first review. I have a non-trivial change, namely changing the shape of the matrices at the beginning of the proof to avoid...
There is https://github.com/mituharu/math-comp/pull/1 that should be taken into account (i.e. merged before the second review).
I am quite confused, I got rid of the commits for the previous PRs and rebased on top of master, it should be correct now.
Sad, I hoped I could avoid compiling myself...
The CI does too, does it not ?
Yes, but a lot of them do not need `algebra`. The ones who do were skipped (as far as I understand).
Is there something left to do here, beyond rebasing?
I think so. As an orthogonal matter of fact, I just noticed that we should be able to remove a few more `_.+1` once https://github.com/math-comp/math-comp/pull/1256 is merged.