add two references and fix one (#437)

leanprover-community · Feb 4, 2024 · 6995221 · 6995221
1 parent 5aec6e9
commit 6995221
Showing 1 changed file with 115 additions and 11 deletions.
diff --git a/lean.bib b/lean.bib
@@ -148,19 +148,67 @@ @InProceedings{   BaanenBCD23
   bibsource     = {dblp computer science bibliography, https://dblp.org}
 }
 
-@Misc{            BaanenDahmenNarayananNuccio21,
+@InProceedings{   BaanenDahmenNarayananNuccio21,
+  author        = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni
+                  and N{uccio Mortarino Majno di Capriglio}, Filippo A. E.},
+  title         = {A Formalization of {D}edekind {D}omains an {C}lass
+                  {G}roups of {G}lobal {F}ields},
+  booktitle     = {12th International Conference on Interactive Theorem
+                  Proving (ITP 2021)},
+  pages         = {5:1--5:19},
+  series        = {Leibniz International Proceedings in Informatics
+                  (LIPIcs)},
+  isbn          = {978-3-95977-188-7},
+  issn          = {1868-8969},
+  year          = {2021},
+  volume        = {193},
+  editor        = {Cohen, Liron and Kaliszyk, Cezary},
+  publisher     = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
+  address       = {Dagstuhl, Germany},
+  url           = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.5},
+  urn           = {urn:nbn:de:0030-drops-139004},
+  doi           = {10.4230/LIPIcs.ITP.2021.5},
+  annote        = {Keywords: formal math, algebraic number theory,
+                  commutative algebra, Lean, mathlib},
+  tags          = {formalization, lean3}
+}
+
+@Article{         BaanenDahmenNarayananNuccio22,
+  author        = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni
+                  and N{uccio Mortarino Majno di Capriglio}, Filippo A. E.},
   title         = {A formalization of {D}edekind domains and class groups of
                   global fields},
-  author        = {Anne Baanen and Sander R. Dahmen and Ashvni Narayanan and
-                  Filippo A. E. Nuccio},
-  year          = {2021},
-  eprint        = {2102.02600},
-  archiveprefix = {arXiv},
-  primaryclass  = {cs.LO},
-  url           = {https://arxiv.org/abs/2102.02600},
-  website       = {https://github.com/lean-forward/class-number},
-  tags          = {formalization, lean3},
-  note          = {To be presented at ITP 2021}
+  journal       = {J. Automat. Reason.},
+  fjournal      = {Journal of Automated Reasoning},
+  volume        = {66},
+  year          = {2022},
+  number        = {4},
+  pages         = {611--637},
+  issn          = {0168-7433,1573-0670},
+  mrclass       = {03B35 (11R29 13C20)},
+  mrnumber      = {4505023},
+  doi           = {10.1007/s10817-022-09644-0},
+  url           = {https://doi.org/10.1007/s10817-022-09644-0},
+  tags          = {formalization, lean3}
+}
+
+@Article{         BaanenDahmenNarayananNuccio22,
+  author        = {Baanen, Anne and Dahmen, Sander R. and Narayanan, Ashvni
+                  and N{uccio Mortarino Majno di Capriglio}, Filippo A. E.},
+  title         = {A formalization of {D}edekind domains and class groups of
+                  global fields},
+  journal       = {J. Automat. Reason.},
+  fjournal      = {Journal of Automated Reasoning},
+  volume        = {66},
+  year          = {2022},
+  number        = {4},
+  pages         = {611--637},
+  issn          = {0168-7433,1573-0670},
+  mrclass       = {03B35 (11R29 13C20)},
+  mrnumber      = {4505023},
+  doi           = {10.1007/s10817-022-09644-0},
+  url           = {https://doi.org/10.1007/s10817-022-09644-0},
+  tags          = {formalization, lean3}
 }
 
 @Booklet{         Best2021,
@@ -424,6 +472,62 @@ @InProceedings{   deFrutos23
   tags          = {formalization, lean3}
 }
 
+@InProceedings{   deFrutosNuccio24,
+  author        = {de Frutos-Fern\'{a}ndez, Mar\'{\i}a In\'{e}s and N{uccio
+                  Mortarino Majno di Capriglio, Filippo A. E.}},
+  title         = {A Formalization of Complete Discrete Valuation Rings and
+                  Local Fields},
+  year          = {2024},
+  isbn          = {9798400704888},
+  publisher     = {Association for Computing Machinery},
+  address       = {New York, NY, USA},
+  url           = {https://doi.org/10.1145/3636501.3636942},
+  doi           = {10.1145/3636501.3636942},
+  abstract      = {Local fields, and fields complete with respect to a
+                  discrete valuation, are essential objects in commutative
+                  algebra, with applications to number theory and algebraic
+                  geometry. We formalize in Lean the basic theory of
+                  discretely valued fields. In particular, we prove that the
+                  unit ball with respect to a discrete valuation on a field
+                  is a discrete valuation ring and, conversely, that the adic
+                  valuation on the field of fractions of a discrete valuation
+                  ring is discrete. We define finite extensions of valuations
+                  and of discrete valuation rings, and prove some
+                  localization results. Building on this general theory, we
+                  formalize the abstract definition and some fundamental
+                  properties of local fields. As an application, we show that
+                  finite extensions of the field ℚp of p-adic numbers and
+                  of the field Fp((X)) of Laurent series over Fp are local
+                  fields.},
+  booktitle     = {Proceedings of the 13th ACM SIGPLAN International
+                  Conference on Certified Programs and Proofs},
+  pages         = {190–204},
+  numpages      = {15},
+  keywords      = {mathlib, local fields, formal mathematics, discrete
+                  valuation rings, algebraic number theory, Lean},
+  series        = {CPP 2024},
+  tags          = {formalization, lean3}
+}
+
+@InProceedings{   deFrutosNuccio24,
+  author        = {de Frutos-Fern\'{a}ndez, Mar\'{\i}a In\'{e}s and N{uccio
+                  Mortarino Majno di Capriglio, Filippo A. E.}},
+  title         = {A {F}ormalization of {C}omplete {D}iscrete {V}aluation
+                  {R}ings and {L}ocal {F}ields},
+  year          = {2024},
+  isbn          = {9798400704888},
+  publisher     = {Association for Computing Machinery},
+  address       = {New York, NY, USA},
+  url           = {https://doi.org/10.1145/3636501.3636942},
+  doi           = {10.1145/3636501.3636942},
+  booktitle     = {Proceedings of the 13th ACM SIGPLAN International
+                  Conference on Certified Programs and Proofs},
+  pages         = {190–204},
+  numpages      = {15},
+  series        = {CPP 2024},
+  tags          = {formalization, lean3}
+}
+
 @Misc{            DeMoura15,
   author        = "{de Moura}, Leonardo and Avigad, Jeremy and Kong, Soonho
                   and Roux, Cody",