eng
episciences.org
Logical Methods in Computer Science
1860-5974
2016-06-22
Volume 12, Issue 2
10.2168/LMCS-12(2:7)2016
1639
journal article
Formalized linear algebra over Elementary Divisor Rings in Coq
Guillaume Cano
Cyril Cohen
https://orcid.org/0000-0003-3540-1050
Maxime Dénès
Anders Mörtberg
Vincent Siles
This paper presents a Coq formalization of linear algebra over elementary
divisor rings, that is, rings where every matrix is equivalent to a matrix in
Smith normal form. The main results are the formalization that these rings
support essential operations of linear algebra, the classification theorem of
finitely presented modules over such rings and the uniqueness of the Smith
normal form up to multiplication by units. We present formally verified
algorithms computing this normal form on a variety of coefficient structures
including Euclidean domains and constructive principal ideal domains. We also
study different ways to extend B\'ezout domains in order to be able to compute
the Smith normal form of matrices. The extensions we consider are: adequacy
(i.e. the existence of a gdco operation), Krull dimension $\leq 1$ and
well-founded strict divisibility.
https://lmcs.episciences.org/1639/pdf
Computer Science - Logic in Computer Science
Mathematics - Rings and Algebras
I.2.3
F.4.1