10.2168/LMCS-12(2:7)2016
https://lmcs.episciences.org/1639
Cano, Guillaume
Guillaume
Cano
Cohen, Cyril
Cyril
Cohen
0000-0003-3540-1050
Dénès, Maxime
Maxime
Dénès
Mörtberg, Anders
Anders
Mörtberg
Siles, Vincent
Vincent
Siles
European Commission
243847
Formalisation of Mathematics
Formalized linear algebra over Elementary Divisor Rings in Coq
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.
episciences.org
Computer Science - Logic in Computer Science
Mathematics - Rings and Algebras
I.2.3
F.4.1
arXiv.org - Non-exclusive license to distribute
2023-02-07
2016-06-22
2016-06-22
eng
journal article
arXiv:1601.07472
10.48550/arXiv.1601.07472
1860-5974
2102.02600
10.1007/s10817-022-09644-0
10.4230/lipics.itp.2021.5
10.48550/arxiv.2102.02600
1871.1/21d2c6a3-060e-40c5-a8b9-af1f21c189d0
https://lmcs.episciences.org/1639/pdf
VoR
application/pdf
Logical Methods in Computer Science
Volume 12, Issue 2
Researchers
Students