coq-mathcomp-algebra.opam

opam-version: "2.0"
version: "dev"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"

homepage: "https://math-comp.github.io/"
bug-reports: "https://github.com/math-comp/math-comp/issues"
dev-repo: "git+https://github.com/math-comp/math-comp.git"
license: "CECILL-B"

build: [ make "-C" "mathcomp/algebra" "-j" "%{jobs}%" ]
install: [ make "-C" "mathcomp/algebra" "install" ]
depends: [ "coq-mathcomp-fingroup" { = version } ]

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.algebra"
]
authors: [ "The Mathematical Components team" ]

synopsis: "Mathematical Components Library on Algebra"
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...
"""