Discrete valuation from nontrivial local compactness ($\mathfrak{m}=\pi {\mathcal{O}}_K,|{\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.