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

### License

BSD License

### Topics

- Computer science/Algorithms/Mathematical
- Mathematics/Algebra

### Session Hermite

- Hermite
- Hermite_IArrays

### Depends on

- Echelon Form

### Used by

- Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
- A verified algorithm for computing the Smith normal form of a matrix

### Auto-related entries

- Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
- A verified algorithm for computing the Smith normal form of a matrix
- Gauss-Jordan Algorithm and Its Applications

## Cite

×

Hermite-AFP

    @article{Hermite-AFP,
      author  = {Jose Divasón and Jesús Aransay},
      title   = {Hermite Normal Form},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Hermite.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- Jul 7, 2015 : Isabelle2015