Hermite Normal Form

  1. Aransay Azofra, Jesús María
  2. Divasón Mallagaray, José
Aldizkaria:
Archive of Formal Proofs

ISSN: 2150-914X

Argitalpen urtea: 2015

Alea: 2015

Orrialdeak: 1-54

Mota: Artikulua

GOOGLE SCHOLAR lock_openSarbide irekia editor

Beste argitalpen batzuk: Archive of Formal Proofs

Lotura duten proiektuak

Formalización de las matemáticas: aplicaciones en cálculo simbólico y álgebra computacional. Formalization of mathematics. applications to symbolic computation and computer algebra.

2015/00074/001

Laburpena

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.