Guillaume Cano ; Cyril Cohen ; Maxime Dénès ; Anders Mörtberg ; Vincent Siles - Formalized linear algebra over Elementary Divisor Rings in Coq

lmcs:1639 - Logical Methods in Computer Science, June 22, 2016, Volume 12, Issue 2 - https://doi.org/10.2168/LMCS-12(2:7)2016
Formalized linear algebra over Elementary Divisor Rings in Coq

Authors: Guillaume Cano ; Cyril Cohen ORCID-iD; 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ézout 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.


    Volume: Volume 12, Issue 2
    Published on: June 22, 2016
    Submitted on: November 11, 2014
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Rings and Algebras,I.2.3,F.4.1
    Fundings :
      Source : OpenAIRE Research Graph
    • Formalisation of Mathematics; Funder: European Commission; Code: 243847

    Linked data

    Source : ScholeXplorer IsCitedBy HANDLE 1871.1/21d2c6a3-060e-40c5-a8b9-af1f21c189d0
    Source : ScholeXplorer IsCitedBy DOI 10.48550/arxiv.2102.02600
    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.itp.2021.5
    Source : ScholeXplorer IsCitedBy ARXIV 2102.02600
    • 1871.1/21d2c6a3-060e-40c5-a8b9-af1f21c189d0
    • 10.48550/arxiv.2102.02600
    • 10.4230/lipics.itp.2021.5
    • 2102.02600
    A formalization of Dedekind domains and class groups of global fields
    Baanen, Anne ; Dahmen, Sander R. ; Narayanan, Ashvni ; Di Capriglio, Filippo A.E.Nuccio Mortarino Majno ; Cohen, Liron ; Kaliszyk, Cezary ;

    7 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 593 times.
    This article's PDF has been downloaded 463 times.