Nontrivial valuation in the local compactness criterion (source code)

= Nontrivial valuation in the local compactness criterion

An infinite field with the trivial <absolute value on a field> is discrete, hence locally compact, but its <residue field> is the original infinite field. Thus local compactness forces a finite <residue field> and a discrete nontrivial value group only when the <valuation> is assumed nontrivial.