Matrix Canonical Forms

This library builds on Mathematical Components and CoqEAL to provide formal proofs in Coq about matrices: the existence of Smith normal forms, Jordan normal forms, etc., converging towards a proof of the Perron-Frobenius theorem.

Meta

• Author(s):
  • Guillaume Cano (initial)
• Coq-community maintainer(s):
  • Yves Bertot (@ybertot)
• License: MIT License
• Compatible Coq versions: 8.10 or later
• Additional dependencies:
  • MathComp ssreflect 1.12 or later
  • MathComp fingroup
  • MathComp algebra
  • MathComp real-closed 1.1.2 or later
  • CoqEAL 1.0.5 or later
• Coq namespace: matrix_canonical_forms
• Related publication(s):
  • Interaction entre algèbre linéaire et analyse en formalisation des mathématiques

Building and installation instructions

To build and install, do:

git clone https://github.com/coq-community/matrix_canonical_forms.git
cd matrix_canonical_forms
make   # or make -j <number-of-cores-on-your-machine>
make install

Documentation

For more information about the project, see the website.