Formal Laurent series $K((x))$, their order, derivative, and residue

For a field $K$, a formal Laurent series is a coefficient function $a:\mathbb{Z}\to K$ whose support is bounded below. Write

$K((x)):=\{{\sum }_{n\ge N}{a}_n{x}^n:N\in \mathbb{Z}\}\mathrm{.}$

Addition is coefficientwise and multiplication is finite convolution in each degree. If the supports of two factors are bounded below by $p$ and $q$, then their product is bounded below by $p+q$, and a fixed coefficient has only finitely many contributing pairs. For nonzero $f$, define

$v_x(f):=\min \{n\in \mathbb{Z}:[x^n]f\mathrm{\ne }0\},$

and set $v_x(0)=+\mathrm{\infty }$. Define $D(x^n)=n{x}^{n-1}$ for every integer $n$, extending coefficientwise, and define the formal residue

${\mathrm{res}}_x(f):=[x^{-1}]f\mathrm{.}$

This generalizes the real-coefficient construction of The formal Laurent series $\mathbb{R}((t^{-1}))$: support bounded below, valuation, leading coefficient and uses the same finite-convolution and least-support conventions proved in $\mathbb{R}((t^{-1}))$ is a commutative ring: the product is a finite sum and both operations preserve support bounded below and Valuation and leading coefficient in $\mathbb{R}((t^{-1}))$: $v(fg)=v(f)+v(g)$, and the behaviour of $v$ under sums. It changes the indeterminate notation from that page's $t^{-1}$ to $x$.