formatting

leanprover-community · Feb 4, 2024 · 51a8be8 · 51a8be8
1 parent f87b033
commit 51a8be8
Showing 1 changed file with 57 additions and 55 deletions.
diff --git a/lean.bib b/lean.bib
@@ -148,61 +148,63 @@ @InProceedings{   BaanenBCD23
   bibsource     = {dblp computer science bibliography, https://dblp.org}
 }
 
-@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 Dedekind Domains and Class Groups of Global Fields}},
-  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},
-  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},
-}
-
-@inproceedings{deFNuc,
-  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},
-  location = {<a class="clickandreadBtn" title="Ressource found in  UNPAYWALL" href="https://dl.acm.org/doi/pdf/10.1145/3636501.3636942" target="_blank" draggable="false"><img src="data:image/svg+xml;base64,PHN2ZyBpZD0iQ2FscXVlXzEiIGRhdGEtbmFtZT0iQ2FscXVlIDEiIHhtbG5zPSJodHRwOi8vd3d3LnczLm9yZy8yMDAwL3N2ZyIgdmlld0JveD0iMCAwIDUwIDI4LjE4Ij48cmVjdCB3aWR0aD0iNTAiIGhlaWdodD0iMjguMTgiIHJ4PSIxNC4wOSIgc3R5bGU9ImZpbGw6IzIxY2UyMSIvPjxwYXRoIGQ9Ik0xOC45MywxNi40NWEuMzIuMzIsMCwwLDAtLjU0LjIydjJoLTRhNS4wOCw1LjA4LDAsMCwxLDAtMTAuMTZoNS4yMlY1LjQ0SDE0LjQ0YTguMTQsOC4xNCwwLDAsMCwwLDE2LjI4aDR2MmEuMzIuMzIsMCwwLDAsLjU0LjIzbDMuNTEtMy41MWEuMzQuMzQsMCwwLDAsMC0uNDZaIiBzdHlsZT0iZmlsbDojZmZmIi8+PHBhdGggZD0iTTQyLjUyLDIxLjA3bC00Ljg0LTUuNjlhMCwwLDAsMCwxLDAsMCw1LjMsNS4zLDAsMCwwLDIuNTktNC45LDUuNDMsNS40MywwLDAsMC01LjQ4LTVIMjguNDhhMCwwLDAsMCwwLDAsMFYyMS42OWEwLDAsMCwwLDAsMCwwaDMuMDVsMCwwVjguNTVzMCwwLDAsMEgzNWEyLjI0LDIuMjQsMCwwLDEsMi4yMiwyLjUzLDIuMywyLjMsMCwwLDEtMi4zMiwySDMyLjRhLjM2LjM2LDAsMCwwLS4yOC41OWw2LjYyLDcuNzlhLjkzLjkzLDAsMCwwLC42OC4zMWgyLjgxQS4zOS4zOSwwLDAsMCw0Mi41MiwyMS4wN1oiIHN0eWxlPSJmaWxsOiNmZmYiLz48Y2lyY2xlIGN4PSIyNC4yIiBjeT0iOC4yIiByPSIyLjc2IiBzdHlsZT0iZmlsbDojZmZmIi8+PC9zdmc+" width="27"></a><conf-loc>, <city>London</city>, <country>UK</country>, </conf-loc>},
-  series = {CPP 2024},
-  tags = {formalization, lean3},
+@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},
+  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},
+}
+
+@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},
 }