Formal power series module (source code)

= Formal power series module
{title2=$M[[t]]$}

For a <vector space> $M$ over a <field> $k$, its formal power series module is $M[[t]]=\varprojlim_n M\otimes_k k[t]/(t^n)$. It is complete for the filtration by $t^nM[[t]]$. The ordinary <tensor product> $M\otimes_k k[[t]]$ embeds in it and consists of series whose coefficients span a finite-dimensional <vector subspace>; it equals $M[[t]]$ if $M$ is finite-dimensional. The inclusion is proper for infinite-dimensional $M$, as shown by a series with linearly independent coefficients.