### Abstract

This work presents a formal proof in Isabelle/HOL of an algorithm to transform a matrix into its Smith normal form, a canonical matrix form, in a general setting: the algorithm is parameterized by operations to prove its existence over elementary divisor rings, while execution is guaranteed over Euclidean domains. We also provide a formal proof on some results about the generality of this algorithm as well as the uniqueness of the Smith normal form. Since Isabelle/HOL does not feature dependent types, the development is carried out switching conveniently between two different existing libraries: the Hermite normal form (based on HOL Analysis) and the Jordan normal form AFP entries. This permits to reuse results from both developments and it is done by means of the lifting and transfer package together with the use of local type definitions.

### License

BSD License

### Topics

- Mathematics/Algebra
- Computer science/Algorithms/Mathematical

### Session Smith_Normal_Form

- Smith_Normal_Form
- Diagonal_To_Smith
- Mod_Type_Connect
- SNF_Missing_Lemmas
- Cauchy_Binet
- Smith_Normal_Form_JNF
- Rings2_Extended
- Finite_Field_Mod_Type_Connection
- Admits_SNF_From_Diagonal_Iff_Bezout_Ring
- SNF_Uniqueness
- Cauchy_Binet_HOL_Analysis
- Diagonalize
- SNF_Algorithm_Two_Steps
- Diagonal_To_Smith_JNF
- SNF_Algorithm_Two_Steps_JNF
- SNF_Algorithm
- SNF_Algorithm_HOL_Analysis
- Elementary_Divisor_Rings
- SNF_Algorithm_Euclidean_Domain
- Smith_Certified
- Alternative_Proofs

### Depends on

- The Factorization Algorithm of Berlekamp and Zassenhaus
- Hermite Normal Form
- List Index
- Perron-Frobenius Theorem for Spectral Radius Analysis

### Used by

- Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation

### Auto-related entries

- Extension of Types-To-Sets
- Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation

## Cite

×

Smith_Normal_Form-AFP

    @article{Smith_Normal_Form-AFP,
      author  = {Jose Divasón},
      title   = {A verified algorithm for computing the Smith normal form of a matrix},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Smith_Normal_Form.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
- May 25, 2020 : Isabelle2020