-
Notifications
You must be signed in to change notification settings - Fork 8
/
Copy pathmeta.yml
149 lines (127 loc) · 4.76 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
fullname: Abel - Ruffini Theorem as a Mathematical Component
shortname: abel
organization: math-comp
opam_name: coq-mathcomp-abel
community: false
action: true
coqdoc: false
synopsis: >-
Abel - Ruffini's theorem
description: |-
This repository contains a proof of Abel - Galois Theorem
(equivalence between being solvable by radicals and having a
solvable Galois group) and Abel - Ruffini Theorem (unsolvability of
quintic equations) in the Coq proof-assistant and using the
Mathematical Components library.
authors:
- name : Sophie Bernard
initial: true
- name: Cyril Cohen
initial: true
- name: Assia Mahboubi
initial: true
- name: Pierre-Yves Strub
initial: true
publications:
- pub_url: https://hal.inria.fr/hal-03136002
pub_title: >
Unsolvability of the Quintic Formalized in
Dependent Type Theory
opam-file-maintainer: Cyril Cohen <[email protected]>
opam-file-version: dev
license:
fullname: CeCILL-B
identifier: CECILL-B
file: CeCILL-B
supported_coq_versions:
text: Coq 8.10 to 8.16
opam: '{ (>= "8.10" & < "8.20~") | = "dev" }'
tested_coq_opam_versions:
- version: 'coq-dev'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.19'
repo: 'mathcomp/mathcomp-dev'
- version: 'coq-8.18'
repo: 'mathcomp/mathcomp-dev'
- version: '2.2.0-coq-8.19'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.18'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.17'
repo: 'mathcomp/mathcomp'
- version: '2.1.0-coq-8.16'
repo: 'mathcomp/mathcomp'
dependencies:
- opam:
name: coq-mathcomp-ssreflect
version: '{ (>= "2.0.0" & < "2.3~") | = "dev" }'
description: |-
[MathComp ssreflect 2.0 and later](https://math-comp.github.io)
- opam:
name: coq-mathcomp-fingroup
description: |-
[MathComp fingroup](https://math-comp.github.io)
- opam:
name: coq-mathcomp-algebra
description: |-
[MathComp algebra](https://math-comp.github.io)
- opam:
name: coq-mathcomp-solvable
description: |-
[MathComp solvable](https://math-comp.github.io)
- opam:
name: coq-mathcomp-field
description: |-
[MathComp field](https://math-comp.github.io)
- opam:
name: coq-mathcomp-real-closed
version: '{ (>= "2.0.0") | = "dev" }'
description: |-
[MathComp real closed >= 2.0.0](https://github.com/math-comp/real-closed)
namespace: Abel
keywords:
- name: algebra
- name: Galois
- name: Abel Ruffini
- name: unsolvability of quintincs
documentation: |-
## Organization of the code
- `abel.v` itself contains the main theorems:
+ `galois_solvable_by_radical` (requires explicit roots of unity),
+ `ext_solvable_by_radical` (equivalent, and still requires roots of unity),
+ `radical_solvable_ext` (no mention of roots of unity),
+ `AbelGalois`, (equivalence obtained from the above two, requires
roots of unity), and consequences on solvability of polynomial
+ and their consequence on the example polynomial X⁵ -4X + 2:
`example_not_solvable_by_radicals`,
- `xmathcomp/various.v` contains various (rather straightforward)
extensions that should be added to various mathcomp packages asap
with potential minor modifications,
- `xmathcomp/char0.v` contains 0 characteristic specific results,
that could use a refactoring for a smoother integration with
mathcomp. e.g. ratr could get a canonical structure or rmorphism
when the target field is a `lmodType ratr`, and we could provide a
wrapper`NullCharType` akin to `PrimeCharType` (from `finfield.v`),
- `xmathcomp/cyclotomic.v` contains complementary results about
cyclotomic polynomials,
- `xmathcomp/map_gal.v` contains complementary results about galois
groups and galois extensions, including various isomorphisms,
minimal galois extensions, solvable extensions, and mapping galois
groups and galois extensions from a splitting field to
another. This last construction is essential in switching to
fields with roots of unity when we do not have them yet,
- `xmathcomp/classic_ext.v` contains the theory of classic
extensions by arbitrary polynomials, most of the results there are
in the classically monad, making the results available either for
a boolean goal or a classical goal. This was instrumental in
eliminating references to some embarrassing roots of the unity.
- `xmathcomp/algR.v` contains a proof that the real subset of `algC`
(isomorphic to `{x : algC | x \is Num.real}`) is a real closed field
(and archimedean), and endows this type `algR` with appropriate
canonical instances.
- `xmathcomp/real_closed_ext.v` contains some missing lemmas from
the library `math-comp/real_closed`, in particular bounding the
number of real roots of a polynomial by one plus the number of
real roots of its derivative,
## Development information
[Developping with nix](NIX.md)