Inversion in the formal power series ring In my lecture a (commutative algebra) theorem was given without proof:
Let $R$ be a commutative ring and $p\in R[[x]]$ such that $p(0)=0$. Then we have 

$\exists q\in R[[x]]:p(q(x))=q(p(x))=x\quad\Leftrightarrow\quad p'(0)\in R^{\times}.$

Since I have not seen a proof I am interested in references about this. So who knows some books/papers/...?
Thank you.
 A: That's a variant of the following famous result:

Theorem (Hensel's Lemma): Let $S$ be an $I$-adically complete commutative ring, $f\in S[T]$ and $\xi\in S$ such that $f(\xi)\equiv 0$ modulo $I$ (i.e. $\xi$ is an 'approximate' zero of $f$) and $f^{\prime}(\xi)\in (S/I)^\times$. Then there exists a unique $\tilde{\xi}$ such that $\xi\equiv\tilde{\xi}$ modulo $I$ such that $f(\xi)=0$. 

Proof: This can be proved by mimicking Newton's Method, with convergence ensured by $I$-completeness.
Now, in the above formulation, $p$ is (necessarily) a polynomial and not a power series, but if you restrict the evaluation function to elements of $I$, you can allow $f\in S[[T]]$ and interpret it as an operator $I\to I$. This results in a well-posed question which is again answered affirmatively by Newton's Method.
To get to your problem, apply the theorem in the following context: $$S:=R[[x]], \quad I := (x),\quad \xi:=0,\quad\text{ and }\quad f := p(T) - x\in R[[x]][[T]]$$
Note that $x$ is interpreted as a constant term here. The assumptions of the theorem are met, $$f(0) = -x\in I\quad\text{ and }\quad f^{\prime}(0) = p^{\prime}(0)\in R^{\times}\subset R[[x]]^{\times},$$ so we conclude the existence of $q\in (x)\subset R[[x]]$ such that $f(q)=0$, i.e. $p(q) = x$. 
Finally, comparing the coefficients of $x$ in $p(q)=x$ shows that $p^{\prime}(0)q^{\prime}(0)=1$, so $q$ satisfies the same hypothesis as $p$. This shows that $\{p\in x R[[x]]\ |\ p^{\prime}(0)\in R^{\times}\}$ is a group under substitution, with unit element $x$, and the uniqueness of inverses shows that $p(q)=x$ implies $q(p)=x$, too.
