### Abstract

We formalize an algorithm to compute the Echelon Form of a matrix. We have proved its existence over Bézout domains and made it executable over Euclidean domains, such as the integer ring and the univariate polynomials over a field. This allows us to compute determinants, inverses and characteristic polynomials of matrices. The work is based on the HOL-Multivariate Analysis library, and on both the Gauss-Jordan and Cayley-Hamilton AFP entries. As a by-product, some algebraic structures have been implemented (principal ideal domains, Bézout domains...). The algorithm has been refined to immutable arrays and code can be generated to functional languages as well.

BSD License### Topics

### Theories of Echelon_Form

- Rings2
- Cayley_Hamilton_Compatible
- Code_Cayley_Hamilton
- Echelon_Form
- Echelon_Form_Det
- Echelon_Form_Inverse
- Examples_Echelon_Form_Abstract
- Echelon_Form_IArrays
- Echelon_Form_Det_IArrays
- Code_Cayley_Hamilton_IArrays
- Echelon_Form_Inverse_IArrays
- Examples_Echelon_Form_IArrays