Complete discretely valued field (source code)

= Complete discretely valued field
{title2=$v:F^\times\to\mathbb Z$}

A <field> with a surjective discrete <valuation>, complete for the associated non-Archimedean metric. Its <valuation ring> is a <discrete valuation ring>, and its <maximal ideal> is generated by a <uniformizer>. <Completeness> allows successive congruence solutions to converge to actual roots, which underlies the <Hensel lemma>. Non-Archimedean <local fields> are examples; <completeness> alone does not require the <residue field> to be finite.