This is a formal matrix library in Coq, and integrated with multiple different implementations. Our goal is to provide a unified framework for different implementations of formalized matrix libraries, so as to decouple the differences between underlying technologies and upper-level applications.
opam install coq-matrix
Below are main links of this project: