Discrete valuation from nontrivial local compactness (source code)

= Discrete valuation from nontrivial local compactness
{title2=$\mathfrak m=\pi\mathcal O_K,\quad|\mathcal O_K/\mathfrak m|<\infty$}

For a locally compact field with a nontrivial <Non-Archimedean absolute value>, scaling a compact neighborhood makes its <valuation ring> compact. Its open <maximal ideal> gives a finite discrete <residue field>, so that ideal is also closed and compact. A nonzero element of maximal absolute value in the ideal generates it. Successive division by this <uniformizer> makes the value group discrete.