Package coq-finmatrix.1.0.0

[zhengpushi]

FinMatrix is a formal matrix library in Coq, which we started from finite sets (over natural numbers), vector 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, an inversion method based on Gaussian Elimination;
• minvAM, an inversion technique utilizing the Adjoint Matrix method.
  The main features of this library is:
• Support for directly evaluation in Coq, including for minvGE or minvAM.
• Extracted OCaml code is clear and readable (free of obfuscated magic.obj code)
• Support Leibniz equality of vectors or matrices
• Intrinsic support for nested vectors of high rank.
  The HTML document and dependent-graph can be found in homepage: FinMatrix .