Formalized linear algebra over Elementary Divisor Rings in Coq
From MaRDI portal
Publication:5739892
DOI10.2168/LMCS-12(2:7)2016zbMath1448.68461arXiv1601.07472MaRDI QIDQ5739892
Cyril Cohen, Anders Mörtberg, Vincent Siles, Maxime Dénès, Guillaume Cano
Publication date: 6 July 2016
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1601.07472
15B33: Matrices over special rings (quaternions, finite fields, etc.)
68V20: Formalization of mathematics in connection with theorem provers
Uses Software