A formalization of the Smith normal form in higher-order logic

DOI10.1007/s10817-022-09631-5MaRDI QIDQ2102950

Jose Divasón, René Thiemann

Publication date: 12 December 2022

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-022-09631-5

zbMATH Keywords

theorem proving; Isabelle/HOL; elementary divisor rings; local type definitions

Mathematics Subject Classification ID

15B33: Matrices over special rings (quaternions, finite fields, etc.)

13F10: Principal ideal rings

15A21: Canonical forms, reductions, classification

68V20: Formalization of mathematics in connection with theorem provers

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Uses Software

• ACL2
• Coq
• Isabelle
• Isabelle/HOL
• PVS
• Mizar
• Kenzo
• HOL Light
• Locales
• Transfer
• Lifting
• MathOverflow
• Echelon Form
• Cayley-Hamilton
• Berlekamp Zassenhaus
• Archive Formal Proofs
• Modular_arithmetic_LLL_and_HNF_algorithms
• Smith_Normal_Form
• Hermite
• Smooth_Manifolds