Formalized linear algebra over Elementary Divisor Rings in Coq
From MaRDI portal
Publication:5739892
DOI10.2168/LMCS-12(2:7)2016zbMath1448.68461arXiv1601.07472OpenAlexW3104555329MaRDI QIDQ5739892
Maxime Dénès, Vincent Siles, Guillaume Cano, Cyril Cohen, Anders Mörtberg
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
Matrices over special rings (quaternions, finite fields, etc.) (15B33) Formalization of mathematics in connection with theorem provers (68V20)
Related Items (6)
Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL ⋮ Using abstract stobjs in ACL2 to compute matrix normal forms ⋮ A Formal Proof of the Computation of Hermite Normal Form in a General Setting ⋮ Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem ⋮ A formalization of Dedekind domains and class groups of global fields ⋮ A formalization of the Smith normal form in higher-order logic
Uses Software
This page was built for publication: Formalized linear algebra over Elementary Divisor Rings in Coq
