The valuation ring and local compactness. The opening, unlettered requests use
The ultrametric inequality makes a valuation ring; its elements outside are exactly the units, so is its unique maximal ideal, and is the residue field.
Here the customary nontrivial-valuation hypothesis for a local field is necessary. With the trivial absolute value, any infinite field is discrete and locally compact, but its residue field is infinite and there is no nonzero uniformizer. We use the nontrivial valuation in the conclusions below.
Local compactness first gives a compact neighborhood of zero. Choose a sufficiently small nonzero so that the closed set is contained in that compact neighborhood. Then , and hence , is compact. Since is open, its cosets give a discrete compact quotient , which must be finite. Write . The subgroup now has finite index and is closed in , hence compact. The continuous function attains on a maximum with . Choose with . Every has , so
Successive division by shows that every nonzero element of is a unit times a power of : division must terminate because . Thus the value group is discrete. A Cauchy sequence eventually lies in a translate of the compact ring , has a convergent subsequence, and consequently converges itself. These arguments prove the discrete valuation from nontrivial local compactness and the completeness of locally compact nontrivially valued fields.
The iterated-power limit. Normalize the discrete valuation by , and write , where is the residue characteristic. For with , the binomial theorem gives
The linear term gains a factor (or is zero in positive characteristic), while all terms of degree at least two have valuation at least .
For , reduction gives , because has order . Iterating the inequality yields
The sequence is Cauchy and converges to a unit . Since the reduction of is always , its limit has the same residue. Taking limits after shifting the sequence gives , whence
This is the Teichmuller representative. The Hensel lemma applied to , whose derivative is a unit at every nonzero residue, shows uniqueness for each residue. Consequently the prime-to- roots give a canonical splitting