A Formalization of Complete Discrete Valuation Rings and Local Fields

Explore a comprehensive formalization of complete discrete valuation rings and local fields in this 27-minute conference talk from CPP 2024. Delve into the basic theory of discretely valued fields, proving that the unit ball with respect to a discrete valuation on a field is a discrete valuation ring and that the adic valuation on the field of fractions of a discrete valuation ring is discrete. Learn about finite extensions of valuations and discrete valuation rings, as well as localization results. Discover the abstract definition and fundamental properties of local fields, with applications demonstrating that finite extensions of p-adic numbers and Laurent series over finite fields are local fields. Gain insights into formal mathematics using Lean and mathlib, with implications for algebraic number theory and algebraic geometry.

[CPP'24] A Formalization of Complete Discrete Valuation Rings and Local Fields