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 global-to-local 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 $\mathbb{Q}_p$ of $p$-adic numbers and of the field $\mathbb{F}_p(\!(X)\!)$ of Laurent series over $\mathbb{F}_p$ are local fields.

翻译：局部域以及关于离散赋值完备的域是交换代数中的基本对象，在数论和代数几何中均有应用。我们在Lean中形式化了离散赋值域的基础理论。特别地，我们证明了域上关于离散赋值的单位球是一个离散赋值环，反之，离散赋值环的分式域上的adic赋值是离散的。我们定义了赋值和离散赋值环的有限扩张，并证明了一些整体-局部结果。在此一般理论的基础上，我们形式化了局部域的抽象定义及其一些基本性质。作为应用，我们证明了$p$-进数域$\mathbb{Q}_p$和$\mathbb{F}_p$上的Laurent级数域$\mathbb{F}_p(\!(X)\!)$的有限扩张是局部域。