  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.
