全局域的戴德金域与类群的形式化
计算机科学中的逻辑
2022-08-31 v4 数论
摘要
戴德金域（Dedekind domains）及其类群是交换代数中的概念，在代数数论中至关重要。我们作为 mathlib 数学库的一部分，在 Lean 证明器中形式化了这些结构及若干基本性质，包括类群的数论有限性结果。本文描述了形式化过程，指出了在开发中发现的实用惯用法以及该项目涉及的 mathlib 去中心化协作流程。
引用
@article{arxiv.2102.02600,
title = {A formalization of Dedekind domains and class groups of global fields},
author = {Anne Baanen and Sander R. Dahmen and Ashvni Narayanan and Filippo A. E. Nuccio},
journal= {arXiv preprint arXiv:2102.02600},
year = {2022}
}
备注
Expanded version of https://drops.dagstuhl.de/opus/volltexte/2021/13900/ (appeared ar in the Leibniz International Proceedings in Informatics - Conference Interactive Theorem Proving 2021 (Rome, Italy)). To appear in the Journal of Automated Reasoning