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 theore...
Main Authors: | , , , , |
---|---|
Format: | Article |
Language: | English |
Published: |
Logical Methods in Computer Science e.V.
2016-06-01
|
Series: | Logical Methods in Computer Science |
Subjects: | |
Online Access: | https://lmcs.episciences.org/1639/pdf |