Prescribed ramification and residue degree for a Laurent series field (source code)

= Prescribed ramification and residue degree for a Laurent series field
{title2=$\mathbb F_{p^f}((u))/\mathbb F_p((t)),\quad t=u^e$}

For arbitrary positive integers $e,f$, the displayed extension has degree $ef$, <ramification index> $e$, and <residue degree> $f$. If $|t|=p^{-1}$, its unique extended <absolute value on a field> is $|\sum a_nu^n|=p^{-\min\{n:a_n\ne0\}/e}$. A basis consists of $\gamma_i u^j$, where the $\gamma_i$ form an <basis> of $\mathbb F_{p^f}$ and $0\le j<e$. Regrouping a Laurent series by its exponent modulo $e$ proves the basis assertion. When $p$ divides $e$ the extension can be inseparable; the valuation calculation still applies.