We use the proof assistant Isabelle2019 https://isabelle.in.tum.de/.
To use the library download the Archive of Formal Proofs (https://www.isa-afp.org/download.html) or at least the following entries:
- https://www.isa-afp.org/entries/Jordan_Normal_Form.html
- https://www.isa-afp.org/entries/Matrix_Tensor.html
- https://www.isa-afp.org/entries/VectorSpace.html
To learn more about the project please visit the dedicated stream on the Isabelle Zulip chat https://isabelle.zulipchat.com/.