A formalization of Dedekind domains and class groups of global fields

DOI10.1007/S10817-022-09644-0MaRDI QIDQ2102929zbMATH OpenOpenAlexFDO

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

Publication date 12 December 2022

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

Copyright license Creative Commons Attribution 4.0 International

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)

Recommendations

• scientific article; zbMATH DE number 7699422
• Graded rings in Lean's dependent type theory
• Factorization of prime ideal extensions in Dedekind domains
• Formalizing Galois theory
• Schemes in Lean

Cites work

• scientific article; zbMATH DE number 1703931 (Why is no real title available?)
• scientific article; zbMATH DE number 3133601 (Why is no real title available?)
• scientific article; zbMATH DE number 47996 (Why is no real title available?)
• scientific article; zbMATH DE number 1970438 (Why is no real title available?)
• scientific article; zbMATH DE number 7568174 (Why is no real title available?)
• scientific article; zbMATH DE number 7699422 (Why is no real title available?)
• A Uniform Proof of the Finiteness of the Class Group of a Global Field
• Algebraic numbers
• Axiomatic characterization of fields by the product formula for valuations
• Canonical structures for the working Coq user
• Construction of real algebraic numbers in Coq
• Every Abelian group is a class group
• Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem
• Formalized linear algebra over elementary divisor rings in \textsc{Coq}
• Nine Chapters of Analytic Number Theory in Isabelle/HOL.
• The Lean theorem prover (system description)

Cited in

(5)

• A Uniform Proof of the Finiteness of the Class Group of a Global Field
• A formalization of all notions in the statement of a theorem by Deligne
• Graded rings in Lean's dependent type theory
• A formalization of Dedekind domains and class groups of global fields
• Mathematics and the formal turn

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2102929)