Local compactness criterion for a complete non-Archimedean field (source code)

= Local compactness criterion for a complete non-Archimedean field

A complete non-Archimedean valued field is locally compact exactly when its valuation is discrete and its residue field is finite. In that case its valuation ring is the inverse limit of the finite rings $\mathcal O/\mathfrak m^n$ and is compact.