A Formalization of Dedekind Domains and Class Groups of Global Fields

Autor: Baanen, Anne, Dahmen, Sander R., Narayanan, Ashvni, Di Capriglio, Filippo A.E.Nuccio Mortarino Majno, Cohen, Liron, Kaliszyk, Cezary

Publikováno v: 12th International Conference on Interactive Theorem Proving (ITP 2021)
12th International Conference on Interactive Theorem Proving (ITP 2021), Jun 2021, Rome, Italy. ⟨10.4230/LIPIcs.ITP.2021.5⟩
Baanen, A, Dahmen, S R, Narayanan, A & Di Capriglio, F A E N M M 2021, A formalization of Dedekind domains and class groups of global fields . in L Cohen & C Kaliszyk (eds), 12th International Conference on Interactive Theorem Proving (ITP 2021) ., 5, Leibniz International Proceedings in Informatics, LIPIcs, vol. 193, Schloss Dagstuhl-Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 1-19, 12th International Conference on Interactive Theorem Proving, ITP 2021, Virtual, Rome, Italy, 29/06/21 . https://doi.org/10.4230/LIPIcs.ITP.2021.5
Baanen, A, Dahmen, S R, Narayanan, A & Nuccio Mortarino Majno di Capriglio, F A E 2022, ' A Formalization of Dedekind Domains and Class Groups of Global Fields ', Journal of Automated Reasoning, vol. 66, no. 4, pp. 611-637 . https://doi.org/10.1007/s10817-022-09644-0
12th International Conference on Interactive Theorem Proving (ITP 2021), 1-19
STARTPAGE=1;ENDPAGE=19;TITLE=12th International Conference on Interactive Theorem Proving (ITP 2021)
Journal of Automated Reasoning, 66(4), 611-637. Springer Netherlands

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 group

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9bb17d640edab8c278236475e1f0392c