To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

FORMALIZED LINEAR ALGEBRA… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on


Journal article
Authors G. Cano
C. Cohen
M. Denes
Anders Mörtberg
Vincent Siles
Published in Logical Methods in Computer Science
Volume 12
Issue 2
ISSN 1860-5974
Publication year 2016
Published at Department of Computer Science and Engineering, Computing Science, Programming Logic
Language en
Keywords Formalization of mathematics, Constructive algebra, COQ, SSREFLECT, smith normal-form, homological algebra, matrices, Computer Science, Science & Technology - Other Topics
Subject categories Computer and Information Science


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 Bezout 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 <= 1 and well-founded strict divisibility.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?