A formalization of Dedekind domains and class groups of global fields

TL;DR

This paper details the formalization of Dedekind domains and class groups within the Lean proof assistant, emphasizing the process, collaboration, and foundational properties relevant to algebraic number theory.

Contribution

It introduces a comprehensive formalization of Dedekind domains and class groups in mathlib, including key properties and collaboration methods.

Findings

Formalized Dedekind domains and class groups in Lean

Proved fundamental properties and finiteness results

Documented collaboration and development process

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.