A formalization of Dedekind domains and class groups of global fields

DOI10.1007/s10817-022-09644-0OpenAlexW3175348509MaRDI QIDQ2102929

Sander R. Dahmen, Anne Baanen, Filippo Nuccio, Ashvni Narayanan

Publication date: 12 December 2022

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

Full work available at URL: https://arxiv.org/abs/2102.02600

zbMATH Keywords

commutative algebraalgebraic number theoryLeanformal mathmathlib

Mathematics Subject Classification ID

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

Related Items (1)

Mathematics and the formal turn

Uses Software

• Isabelle
• KANT/KASH
• PARI/GP
• Isabelle/HOL
• Metamath
• Lean
• Archive Formal Proofs
• Minkowskis_Theorem
• Gaussian_Integers

Cites Work

• Algebraic numbers
• Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem
• Every Abelian group is a class group
• Construction of Real Algebraic Numbers in Coq
• The Lean Theorem Prover (System Description)
• A Uniform Proof of the Finiteness of the Class Group of a Global Field
• Canonical Structures for the Working Coq User
• Formalized linear algebra over Elementary Divisor Rings in Coq
• Axiomatic characterization of fields by the product formula for valuations
• Nine Chapters of Analytic Number Theory in Isabelle/HOL.
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A formalization of Dedekind domains and class groups of global fields