← All papers
A formalization of Dedekind domains and class groups of global fields
cs.LO
Feb 4, 2021 · v2
TL;DR
Formalizes Dedekind domains and class groups of global fields in Lean's mathlib.
Abstract
Dedekind domains and their class groups are notions in commutative algebra that are essential in algebraic number theory. We formalized these structures and fundamental properties, including number theoretic finiteness results for class groups, in the Lean prover as part of the mathlib mathematical library. We describe the formalization process, noting the idioms we found useful in our development and mathlib's decentralized collaboration processes involved in this project.
Problem
Dedekind domains and class groups are essential structures in algebraic number theory, but they had not been formalized in Lean's mathlib library, limiting the ability to build verified algebraic number theory.
Approach
The authors formalize Dedekind domains, their fundamental properties, and finiteness results for class groups of global fields in Lean as part of the mathlib mathematical library. They describe idioms found useful during development and mathlib's decentralized collaboration processes.
Results
The formalization is merged into mathlib, providing a verified foundation for algebraic number theory in Lean. The project demonstrates that decentralized collaboration on large-scale formalizations is feasible within the mathlib ecosystem.