Coherent and Strongly Discrete Rings in Type Theory

DOI10.1007/978-3-642-35308-6_21zbMath1383.03016OpenAlexW150645361MaRDI QIDQ4916066

Vincent Siles, Thierry Coquand, Anders Mörtberg

Publication date: 19 April 2013

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-35308-6_21

zbMATH Keywords

formalization of mathematicsCoqconstructive algebraSSReflect

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Dedekind, Prüfer, Krull and Mori rings and their generalizations (13F05)

Related Items

Linear systems over localizations of rings, Zacharias representation of effective associative rings

Uses Software

• Coq
• Coq/SSReflect