package coq-mathcomp-algebra
Mathematical Components Library on Algebra
Install
Dune Dependency
Authors
Maintainers
Sources
mathcomp-1.17.0.tar.gz
sha256=1779bcdac5d23d90997627364a5943ef4883c6eb54d67ddbb1dfbe6b7795a188
Description
This library contains definitions and theorems about discrete (i.e. with decidable equality) algebraic structures : ring, fields, ordered fields, real fields, modules, algebras, integers, rational numbers, polynomials, matrices, vector spaces...
Tags
keyword:algebra keyword:small scale reflection keyword:mathematical components keyword:odd order theorem logpath:mathcomp.algebraPublished: 09 May 2023
Dependencies (1)
-
coq-mathcomp-fingroup
= version
Dev Dependencies
None
Used by (32)
- coq-addition-chains
- coq-algorand
-
coq-coqeal
>= "1.1.3" - coq-coqeal-theory
-
coq-fcsl-pcm
>= "1.8.0" -
coq-formalv-check_range
= "1.2.0" -
coq-formalv-prim63_mathcomp
= "1.2.0" -
coq-formalv-time
= "1.2.0" -
coq-fourcolor
>= "1.2.5" - coq-fourcolor-reals
- coq-gaia
- coq-gaia-numbers
- coq-gaia-stern
-
coq-graph-theory
>= "0.9.2" - coq-hanoi
-
coq-htt
>= "1.3.0" - coq-htt-core
-
coq-infotheo
>= "0.5.1" & < "0.7.0" - coq-mathcomp-abel
- coq-mathcomp-algebra-tactics
-
coq-mathcomp-analysis
>= "0.3.13" & < "0.5.0" | >= "0.5.2" & < "0.5.4" - coq-mathcomp-apery
- coq-mathcomp-cad
- coq-mathcomp-classical
-
coq-mathcomp-multinomials
>= "1.4" -
coq-mathcomp-real-closed
>= "1.1.3" -
coq-mathcomp-solvable
= "1.17.0" -
coq-mathcomp-sum-of-two-square
>= "1.0.1" - coq-mathcomp-word
- coq-mathcomp-zify
-
coq-matrix
< "1.0.4" -
coq-monae
>= "0.4.5" & < "0.7.0"
Conflicts
None
On This Page