### 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.

### License

### Topics

### Session 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