= Unit criterion for noncommutative formal power series
{title2=$F\text{ is a unit}\iff F_{\varnothing}\ne0$}
A <noncommutative formal power series> over a <field> is a <unit> exactly when its <constant term> is nonzero. Necessity follows because the <constant term> is a <ring homomorphism> to the coefficient <field>. For sufficiency, write $F=c(1+h)$ with $c\ne0$ and $h$ of zero <constant term>. The formal <geometric series> $\sum_{j\geq0}(-h)^j$ is well-defined because only $j\leq d$ can contribute to a <word> of length $d$. Its left and right products with $1+h$ are $1$, by the finite geometric-series identity in each fixed degree. Multiplying by $c^{-1}$ gives the inverse of $F$.
Back to article page
