FinMatrix is a formal matrix library in Coq, which we started from finite sets (over natural numbers), vecotr based on finite sets, and matrices based on vectors. This implementation differs from the CoqMatrix project, which have various models. We have formalized many algebraic and geometric vector or matrix theories, especially including two inversion matrix algorithms: minvGE (inversion based on Gauss Elimination), minvAM (inversion based on Adjoint Matrix).
Below are main links of this project:
We are happy to announce that FinMatrix has been included in the Coq Package Index. Thus, the following command can be used to install this library to your local environment:
opam install coq-finmatrix
The following commands can be used to compile and install this library to your local environment:
make make install
