{rfName}
A

Indexed in

License and use

Citations

Altmetrics

Analysis of institutional authors

De Frutos-Fernández Mi, Nuccio Mortarino Majno Di Capriglio FaeAuthor

Share

Publications
>
Proceedings Paper

A formalization of complete discrete valuation rings and local fields

Publicated to:CPP 2024 - Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with: POPL 2024. 190-204 - 2024-01-09 (), DOI: 10.1145/3636501.3636942

Authors: de Frutos-Fernández, MI; di Capriglio, FAENMM

Affiliations

Univ Autonoma Madrid, Dept Matemat, Madrid, Spain - Author
Univ Jean Monnet St Etienne, Inst Camille Jordan UMR 5208, St Etienne, France - Author
Universidad Autónoma de Madrid - Author
Université Jean Monnet Saint Etienne - Author

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.

Keywords

algebraic number theorydiscrete valuation ringsleanlocal fieldsmathlibAlgebraic number theoryDiscrete valuation ringsFormal mathematicsLeanLocal fieldsMathlib

Quality index

Impact and social visibility

From the perspective of influence or social adoption, and based on metrics associated with mentions and interactions provided by agencies specializing in calculating the so-called "Alternative or Social Metrics," we can highlight as of 2025-06-30:

  • The use, from an academic perspective evidenced by the Altmetric agency indicator referring to aggregations made by the personal bibliographic manager Mendeley, gives us a total of: 2.
  • The use of this contribution in bookmarks, code forks, additions to favorite lists for recurrent reading, as well as general views, indicates that someone is using the publication as a basis for their current work. This may be a notable indicator of future more formal and academic citations. This claim is supported by the result of the "Capture" indicator, which yields a total of: 2 (PlumX).

With a more dissemination-oriented intent and targeting more general audiences, we can observe other more global scores such as:

  • The Total Score from Altmetric: 0.5.
  • The number of mentions on the social network X (formerly Twitter): 1 (Altmetric).

It is essential to present evidence supporting full alignment with institutional principles and guidelines on Open Science and the Conservation and Dissemination of Intellectual Heritage. A clear example of this is:

  • The work has been submitted to a journal whose editorial policy allows open Open Access publication.

Leadership analysis of institutional authors

This work has been carried out with international collaboration, specifically with researchers from: France.

There is a significant leadership presence as some of the institution’s authors appear as the first or last signer, detailed as follows: First Author (DE FRUTOS FERNANDEZ, MARIA INES) .