# Archive of Formal Proofs

The formalizations that we have developed are presented in the Archive of Formal Proofs:

- Perron-Frobenius Theorem for Spectral Radius Analysis
- Hermite Normal Form
- Echelon Form
- QR Decomposition
- Gauss-Jordan Algorithm and Its Applications
- Rank-Nullity Theorem in Linear Algebra

## Gauss - Jordan 2013-2 - Generalized

This development completes the previous one about the Gauss-Jordan algorithm. Now we have generalized some parts of the HOL-Multivariate Analysis library of Isabelle. Above all, we have carried out four kinds of generalizations:

- Lemmas involving real vector spaces are now generalized to vector spaces over any field.
- Some lemmas involving euclidean spaces have been generalized to finite dimensional vector spaces (since the first time that the notion of a finite basis appeared in the library was in the class euclidean_space).
- Lemmas involving real matrices have been generalized to matrices over any field.
- Lemmas about determinants involving the class linordered_idom, such as the lemma "det_identical_columns". These lemmas are now proven using the class comm_ring_1.

- Ranks
- Determinants
- Inverses
- Bases and dimensions of the null space, left null space, column space and row space of a matrix
- Solutions of systems of linear equations (in any case, including systems with one solution, multiple solutions and with no solution)

## Gauss - Jordan 2013-2

This development is based on the previous one about the Gauss-Jordan algorithm, but it has been improved in several ways. Now, the following facts have been formalized and can be computed:

- Ranks
- Determinants
- Inverses
- Bases and dimensions of the null space, left null space, column space and row space of a matrix
- Solutions of systems of linear equations

## Gauss - Jordan

In this development is formalized the well-known Gauss-Jordan algorithm, in order to compute the reduce row echelon form of a matrix. It makes use of the HOL-Multivariate-Analysis session of Isabelle and its matrix representation (function over finite types). We have set up the Isabelle code generator to allow the execution of that representation. In addition, we present an alternative verified type refinement (using nested immutable arrays) that outperforms the original version. Thanks to this algorithm and the Rank Nullity Theorem, ranks and dimensions of some fundamental subspaces can be computed.