A formalization of Dedekind domains and class groups of global fields
From MaRDI portal
Publication:2102929
DOI10.1007/S10817-022-09644-0OpenAlexW3175348509MaRDI QIDQ2102929FDOQ2102929
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)
Full work available at URL: https://arxiv.org/abs/2102.02600
Cites Work
- The Lean Theorem Prover (System Description)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Formalized linear algebra over Elementary Divisor Rings in Coq
- Axiomatic characterization of fields by the product formula for valuations
- Algebraic numbers
- Every Abelian group is a class group
- Title not available (Why is that?)
- Construction of real algebraic numbers in Coq
- Canonical Structures for the Working Coq User
- Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem
- A Uniform Proof of the Finiteness of the Class Group of a Global Field
- Nine Chapters of Analytic Number Theory in Isabelle/HOL.
- Title not available (Why is that?)
Cited In (4)
Uses Software
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)
