Formal power series over a commutative ring and the coefficient-extraction functional $[x^n]$

Let $R$ be a commutative ring. A formal power series over $R$ is a coefficient function $a:\mathbb{N}\to R$, written

$f={\sum }_{n\ge 0}{a}_n{x}^n,$

and $R\mathrm{⟦}x\mathrm{⟧}$ is the set of all such functions. The symbol $x$ is an indeterminate. The notation asserts no analytic convergence and no value of $x$ is being chosen.

For $n\in \mathbb{N}$, the coefficient-extraction functional is evaluation at $n$:

$[x^n]f:=a_n\mathrm{.}$

Define zero and one coefficientwise, put $[x^n](f+g)=[x^n]f+[x^n]g$, and define the Cauchy product by

$[x^n](fg)={\sum }_{i+j=n}[x^i]f[x^j]g={\sum }_{i=0}^n[x^i]f[x^{n-i}]g\mathrm{.}$

The last sum is finite, including when $n=0$. The constant $r\in R$ denotes the series with coefficient $r$ at $0$ and $0$ elsewhere. The series $x$ has coefficient $1$ at $1$ and $0$ elsewhere. Thus $x^0=1$, and $x^n$ is supported at $n$.

The finitely supported coefficient functions form the polynomial part of $R\mathrm{⟦}x\mathrm{⟧}$. Under the coefficient-function definition of The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution, a polynomial is therefore the same data as a finitely supported formal series; the next theorem verifies that this identification respects the ring operations.