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.
翻译：Dedekind 域及其类群是对代数理论至关重要的交替代数概念。 我们正式确定了这些结构和若干基本特性,包括作为数学数学数学图书馆一部分的Lean 证明书中的类群数字理论有限性结果。 本文描述了正规化过程, 指出了我们发现在我们的发展中非常有用的语系以及涉及这个项目的Mathlib 分散化的协作进程。
相关内容
Group一直是研究计算机支持的合作工作、人机交互、计算机支持的协作学习和社会技术研究的主要场所。该会议将社会科学、计算机科学、工程、设计、价值观以及其他与小组工作相关的多个不同主题的工作结合起来，并进行了广泛的概念化。官网链接：https://group.acm.org/conferences/group20/
Arxiv
0+阅读 · 2022年10月18日
Arxiv
0+阅读 · 2022年10月17日
相关主题
相关VIP内容
相关资讯
相关论文
Arxiv
0+阅读 · 2022年10月18日
Arxiv
0+阅读 · 2022年10月17日
微信扫码咨询专知VIP会员