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

BSD License### Depends On

### Used by

### Topics

### Related Entries

### Theories

- 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