Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add two references and fix one #437

Merged
merged 4 commits into from
Feb 4, 2024
Merged

add two references and fix one #437

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
f87b033
added three refs
faenuccio Feb 3, 2024
51a8be8
formatting
faenuccio Feb 4, 2024
2ee5e8e
run bibtool
faenuccio Feb 4, 2024
ab2b57a
added two more refs and run bibtool
faenuccio Feb 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
126 changes: 115 additions & 11 deletions lean.bib
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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",
Expand Down
Loading