Hermite Normal Form

Title:	Hermite Normal Form
Authors:	Jose Divasón and Jesús Aransay
Submission date:	2015-07-07
Abstract:	Hermite Normal Form is a canonical matrix analogue of Reduced Echelon Form, but involving matrices over more general rings. In this work we formalise an algorithm to compute the Hermite Normal Form of a matrix by means of elementary row operations, taking advantage of the Echelon Form AFP entry. We have proven the correctness of such an algorithm and refined it to immutable arrays. Furthermore, we have also formalised the uniqueness of the Hermite Normal Form of a matrix. Code can be exported and some examples of execution involving integer matrices and polynomial matrices are presented as well.
BibTeX:	@article{Hermite-AFP, author = {Jose Divasón and Jesús Aransay}, title = {Hermite Normal Form}, journal = {Archive of Formal Proofs}, month = jul, year = 2015, note = {\url{http://isa-afp.org/entries/Hermite.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Echelon_Form
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.