 Formal power series module

For a vector space $M$ over a field $k$, its formal power series module is $M[[t]]={\underleftarrow{\lim }}_{n}M{\otimes }_{k}k[t]/(t^n)$. It is complete for the filtration by $t^{n}M[[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.