package rocq-mathcomp-algebra
Mathematical Components Library on Algebra
Install
Dune Dependency
Authors
Maintainers
Sources
mathcomp-2.6.0.tar.gz
sha256=b2e8c5c93fdc9bb5ed9b8a06d1c028aa0096a45b1f3ac6c6509d7a6500c72253
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: 24 Jul 2026
Dependencies (3)
-
rocq-micromega-plugin
>= "1.0.0" -
rocq-mathcomp-finite-group
= version -
rocq-mathcomp-order
= version
Dev Dependencies
None
Used by (8)
-
coq-fcsl-pcm
>= "2.3.0" -
coq-mathcomp-algebra
>= "2.6.0" - rocq-mathcomp-classical
- rocq-mathcomp-multinomials
- rocq-mathcomp-real-closed
-
rocq-mathcomp-solvable
>= "2.6.0" - rocq-monae
-
rocq-rouche-capelli
>= "0.2.0"
Conflicts
None
On This Page