Formal Power Series

A formal power series with coefficients in some Ring R 𝑅 R is simply a function a : ℕ → R : 𝑎 → ℕ 𝑅 a:\mathbb{N}\to R , which we want to think of as the coefficients of a (possibly divergent) infinite sum

∑n:ℕan⁢xnsubscript:𝑛ℕsubscript𝑎𝑛superscript𝑥𝑛\par\sum_{n:\mathbb{N}}a_{n}x^{n}

Formal power series form a Ring R ⁢ [ [ X ] ] 𝑅 delimited-[] delimited-[] 𝑋 R[[X]] , where addition is given by

a+b=λ⁢n.an+bnformulae-sequence𝑎𝑏𝜆𝑛subscript𝑎𝑛subscript𝑏𝑛\par a+b=\lambda n.\;a_{n}+b_{n}

and multiplication is given by

a⁢b=λ⁢n.∑k=0nak⁢bn−kformulae-sequence𝑎𝑏𝜆𝑛superscriptsubscript𝑘0𝑛subscript𝑎𝑘subscript𝑏𝑛𝑘\par ab=\lambda n.\;\sum_{k=0}^{n}a_{k}b_{n-k}

which is a sort of Convolution.