A Coq Formalization of Finitely Presented Modules

DOI10.1007/978-3-319-08970-6_13zbMath1416.68157OpenAlexW1044853446MaRDI QIDQ2879252

Cyril Cohen, Anders Mörtberg

Publication date: 8 September 2014

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01378905/file/main.pdf

zbMATH Keywords

homological algebraformalization of mathematicsCoqconstructive algebraSSReflect

Mathematics Subject Classification ID

Uses Software

• Coq
• Coq/SSReflect

This page was built for publication: A Coq Formalization of Finitely Presented Modules