package coq-mathcomp-field
Mathematical Components Library on Fields
Install
Dune Dependency
Authors
Maintainers
Sources
mathcomp-1.12.0.tar.gz
sha256=a57b79a280e7e8527bf0d8710c1f65cde00032746b52b87be1ab12e6213c9783
Description
This library contains definitions and theorems about field extensions, galois theory, algebraic numbers, cyclotomic polynomials...
Tags
keyword:algebra keyword:field keyword:small scale reflection keyword:mathematical components keyword:odd order theorem logpath:mathcomp.fieldPublished: 26 Nov 2020
Dependencies (1)
-
coq-mathcomp-solvable
= version
Dev Dependencies
None
Used by (14)
- coq-geocoq-algebraic
-
coq-infotheo
>= "0.0.7" & < "0.1.1" | >= "0.2.2" & < "0.3.4" | >= "0.5.1" & < "0.6.1" | >= "0.9.3" -
coq-libvalidsdp
= "1.0.0" - coq-mathcomp-abel
-
coq-mathcomp-analysis
>= "0.3.5" & < "0.5.0" | >= "0.5.2" & != "0.5.4" & < "1.16.0" - coq-mathcomp-apery
- coq-mathcomp-cad
-
coq-mathcomp-character
= "1.12.0" -
coq-mathcomp-odd-order
>= "1.12.0" & < "1.14.0" -
coq-mathcomp-real-closed
>= "1.1.2" & < "2.0.6" -
coq-mathcomp-sum-of-two-square
>= "1.0.1" -
coq-monae
>= "0.2.2" & < "0.4" | >= "0.4.5" & < "0.7.0" - coq-robot
-
coq-validsdp
= "1.0.0"
Conflicts
None
On This Page