Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Abel-Galois for any characteristic #83

Open
wants to merge 15 commits into
base: master
Choose a base branch
from
Open

Abel-Galois for any characteristic #83

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
06ea22a
Abel-Galois for any characteristic
Feb 3, 2023
4ab6ab8
fix hornerE changing behaviour between mc versions
Feb 3, 2023
6664b11
update on suggestions
Feb 3, 2023
a57ab3e
byproducts
Apr 21, 2023
959f75d
characteristic independant AbelGalois
Apr 21, 2023
e5b4036
comments
Apr 22, 2023
4848812
remove has_char0 hypotheses
Apr 22, 2023
08606fc
cleanup
Jun 8, 2023
9a91e8a
Simplifications
CohenCyril Apr 27, 2023
d46aedd
set -> pose
CohenCyril Jul 21, 2023
77a6cf7
started cleaning temp
Jul 21, 2023
49fd41e
Merge branch 'AG' of github.com:Tragicus/Abel into AG
Jul 21, 2023
7dff68d
remove duplicate in map_gal; remove temp
Jul 25, 2023
e632d24
refactoring
CohenCyril Jul 25, 2023
51af6b8
shortens a few lines and puts lemmas away
Jul 25, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 3 additions & 1 deletion _CoqProject
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,8 @@ theories/xmathcomp/map_gal.v
theories/xmathcomp/char0.v
theories/xmathcomp/cyclotomic_ext.v
theories/xmathcomp/real_closed_ext.v
theories/xmathcomp/artin_scheier.v
theories/xmathcomp/temp.v

-R theories Abel
-arg -w -arg -projection-no-head-constant
Expand All @@ -15,4 +17,4 @@ theories/xmathcomp/real_closed_ext.v
-arg -w -arg -ambiguous-paths
-arg -w -arg +non-primitive-record
-arg -w -arg +undeclared-scope
-arg -w -arg +implicit-core-hint-db
-arg -w -arg +implicit-core-hint-db
Loading