{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:05Z","timestamp":1753889765717,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2016,6,22]],"date-time":"2016-06-22T00:00:00Z","timestamp":1466553600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["243847"],"award-info":[{"award-number":["243847"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>This paper presents a Coq formalization of linear algebra over elementary\ndivisor rings, that is, rings where every matrix is equivalent to a matrix in\nSmith normal form. The main results are the formalization that these rings\nsupport essential operations of linear algebra, the classification theorem of\nfinitely presented modules over such rings and the uniqueness of the Smith\nnormal form up to multiplication by units. We present formally verified\nalgorithms computing this normal form on a variety of coefficient structures\nincluding Euclidean domains and constructive principal ideal domains. We also\nstudy different ways to extend B\\'ezout domains in order to be able to compute\nthe Smith normal form of matrices. The extensions we consider are: adequacy\n(i.e. the existence of a gdco operation), Krull dimension $\\leq 1$ and\nwell-founded strict divisibility.<\/jats:p>","DOI":"10.2168\/lmcs-12(2:7)2016","type":"journal-article","created":{"date-parts":[[2016,11,21]],"date-time":"2016-11-21T13:47:33Z","timestamp":1479736053000},"source":"Crossref","is-referenced-by-count":9,"title":["Formalized linear algebra over Elementary Divisor Rings in Coq"],"prefix":"10.46298","volume":"Volume 12, Issue 2","author":[{"given":"Guillaume","family":"Cano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3540-1050","authenticated-orcid":false,"given":"Cyril","family":"Cohen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maxime","family":"D\u00e9n\u00e8s","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anders","family":"M\u00f6rtberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vincent","family":"Siles","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2016,6,22]]},"reference":[{"key":"1091:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1639\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1639\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:08:42Z","timestamp":1681243722000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1639"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,22]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-12(2:7)2016","relation":{"is-same-as":[{"id-type":"arxiv","id":"1601.07472","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1601.07472","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2016,6,22]]},"article-number":"1639"}}