package coq-mathcomp-algebra
Mathematical Components Library on Algebra
Install
Dune Dependency
Authors
Maintainers
Sources
mathcomp-2.2.0.tar.gz
sha256=e7e8f3ebfebae10fd290a63fffdbe311d32df7eebc2e66777e194269e72697f5
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:small scale reflection keyword:mathematical components keyword:algebra keyword:algebraic structure hierarchies keyword:archimedean field keyword:floor keyword:ceil keyword:intervals keyword:matrices keyword:vectors keyword:block matrices keyword:determinant keyword:Cramer rule keyword:Vandermonde matrices keyword:LUP decomposition keyword:Gaussian elimination keyword:matrix rank keyword:eigen values keyword:single variable polynomials keyword:bivariate polynomials keyword:polynomial division keyword:integers keyword:rational numbers keyword:semirings keyword:rings keyword:left algebra keyword:left module keyword:unit rings keyword:field keyword:algebraically closed field keyword:additive morphisms keyword:ring morphisms keyword:finite dimensional vector spaces keyword:complex numbers keyword:square root logpath:mathcomp.algebraPublished: 17 Jan 2024
Dependencies (1)
-
coq-mathcomp-fingroup
= version
Dev Dependencies
None
Used by (32)
- coq-addition-chains
- coq-algorand
-
coq-coqeal
>= "2.0.0" - coq-coqeal-theory
-
coq-fcsl-pcm
>= "1.8.0" & < "2.3.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" & < "2.3.0" -
coq-htt-core
< "2.3.0" -
coq-infotheo
>= "0.5.1" & != "0.6.1" & < "0.7.6" | >= "0.9.3" - 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
< "1.16.0" -
coq-mathcomp-multinomials
>= "1.4" & < "2.5.0" -
coq-mathcomp-real-closed
>= "1.1.3" & < "2.0.6" -
coq-mathcomp-solvable
= "2.2.0" -
coq-mathcomp-sum-of-two-square
>= "1.0.1" - coq-mathcomp-word
-
coq-mathcomp-zify
< "1.7.0+2.4+9.0" -
coq-matrix
< "1.0.4" -
coq-monae
>= "0.4.5" & < "0.7.2" - coq-trocq-std-examples
-
rocq-hollight
< "1.1.0" -
rocq-laproof
< "2.0.1"
Conflicts
None
On This Page