Digit expansion with a nonuniformizer (source code)

= Digit expansion with a nonuniformizer
{title2=$x=\sum_{n\geq r}a_n t^n$}

Let a nontrivially valued <local field> have compact <valuation ring> $\mathcal O$, and choose any $t$ with $0<|t|<1$. The quotient $\mathcal O/t\mathcal O$ is finite. A fixed set of representatives containing zero gives every field element a unique convergent digit expansion, with finitely many nonzero negative-index terms. Recursive reduction modulo $t\mathcal O$ gives existence; comparing the first differing digit modulo this ideal gives uniqueness. The element $t$ need not be a <uniformizer>.