A Multivariate polynomial Library for the Mathematical Components Library

This library provides a library for monomial algebra, for multivariate polynomials over ring structures and an extended theory for polynomials whose coefficients range over commutative rings and integral domains.

Meta

• Author(s):
  • Pierre-Yves Strub (initial)
• License: CeCILL-B Free Software License Agreement
• Compatible Rocq/Coq versions: 8.20 or later
• Additional dependencies:
  • MathComp ssreflect 2.4 or later
  • MathComp algebra
  • MathComp bigenough
  • MathComp finmap
• Rocq/Coq namespace: mathcomp.multinomials
• Related publication(s): none

Building and installation instructions

The easiest way to install the latest released version of A Multivariate polynomial Library for the Mathematical Components Library is via OPAM:

opam repo add rocq-released https://rocq-prover.org/opam/released
opam install coq-mathcomp-multinomials

To instead build and install manually, you need to make sure that all the libraries this development depends on are installed. The easiest way to do that is still to rely on opam:

git clone https://github.com/math-comp/multinomials.git
cd multinomials
opam repo add rocq-released https://rocq-prover.org/opam/released
opam install --deps-only .
make   # or make -j <number-of-cores-on-your-machine> 
make install

Credits

Contributors:

• Florent Hivert
• Laurent Thery

This library is also the result of discussions with:

• Sophie Bernard
• Cyril Cohen
• Laurence Rideau