Skip to Main content Skip to Navigation
Journal articles

A formalization of Dedekind domains and class groups of global fields

Abstract : Dedekind domains and their class groups are notions in commutative algebra that are essential in algebraic number theory. We formalized these structures and several fundamental properties, including number theoretic finiteness results for class groups, in the Lean prover as part of the mathlib mathematical library. This paper describes the formalization process, noting the idioms we found useful in our development and mathlib's decentralized collaboration processes involved in this project.
Complete list of metadata
Contributor : Filippo A. E. Nuccio Mortarino Majno Di Capriglio Connect in order to contact the contributor
Submitted on : Monday, August 8, 2022 - 10:12:37 AM
Last modification on : Saturday, September 24, 2022 - 3:36:05 PM


Files produced by the author(s)


  • HAL Id : hal-03355627, version 2


Anne Baanen, Sander R Dahmen, Ashvni Narayanan, Filippo Alberto Edoardo Nuccio Mortarino Majno Di Capriglio. A formalization of Dedekind domains and class groups of global fields. Journal of Automated Reasoning, Springer Verlag, In press. ⟨hal-03355627v2⟩



Record views


Files downloads