Hensel's Lemma and Implicit Function Theorem

Bill Dubuque has largely answered the question, but just to be explict:

Suppose that you have an equation $f(x,y) = 0$, which you want to solve to express $y$ as a function of $x$. (This is a typical implicit function theorem situation.)

Well, the implicit function theorem says that first, you should choose a small n.h. of a point, say $x = 0$ to fix ideas. You should then choose a value $y_0$ of $y$ at this point, i.e. fix a solution to $f(y_0,0) = 0$; again, let's assume that we can take $y_0 = 0$. (In other words, we assume that $f(x,y)$ has no constant term, i.e. that $f(0,0) = 0$.)

Now the implicit function theorem says that we can solve for $y$ locally as a function of $x$ provided that $\dfrac{\partial f}{\partial y}(0,0) \neq 0.$ (Of course, there are other technical assumptions --- $f$ should be smooth and so on; let's ignore those, since in a moment I will take $f$ to be a polynomial.)

Now we could think about the implicit function theorem for analytic functions, and then for formally analytic functions, i.e. for formal power series.

So now the question is: given $f(x,y) = 0$, with $f$ a polynomial with no constant term, when we can find a solution $y \in \mathbb C[[x]]$ with no constant term. A sufficient condition is given by Hensel's lemma: one needs that $f'(0)$ be a unit in $\mathbb C[[x]]$ (thinking of $f$ as a polynomial in $y$ with coeficients in $x$, and taking the derivative in $y$). A formal power series is a unit precisly if its constant term is non-zero, so this can be rephrased as $\dfrac{\partial f}{\partial y}f(0,0) \neq 0,$ which is exactly the same condition as in the implicit function theorem.

In short, Hensel's Lemma in the case of a formal power series ring is exactly the same as an implicit function theorem (for polynomial equations, say) in which one only asks for formal power series solutions.

Incidentally, the connection with Newton's Method is easy to see too:

Suppose that we are trying to solve $f(x,y) = 0$ for $y$ in terms of $x$, under the assumption that $f(0,0) = 0$ and that $\dfrac{\partial f}{\partial y}(0,0) \neq 0.$ We may assume that the latter quantity equals $1$, by rescaling $f$ if necessary, so our equition has the form $$0 = a x + y + b x^2 + c xy + d y^2 + \cdots,$$ which we can rewrite as $$ y = -a x - b x^2 - c x y - d y^2 + \cdots .$$ Note that this already determines $y$ up to second order terms. Now subsitute this expression for $y$ back into the right hand side, to get $$y = - a x - b x^2 - c x (- a x - b x^2 - \cdots) - d (- a x - b x^2 - \cdots)^2 + \cdots,$$ to get $y$ up to third order terms. Now substitute in again, to get $y$ up to fourth order terms, and so on.

This is just Newton's Method.

This proves Hensel's Lemma in this context. It is also easy to estimate the size of the power series coefficients for $y$ that one obtains, and to prove that $y$ has a positive radius of convergence. Thus we also establish a version of the implicit function theorem for analytic functions with the same argument.

Summary: The Implicit Function Theorem, Hensel's Lemma, and Newton's Method are all variants of the same theme.

This is elaborated in various places, e.g. see Kuhlman's paper Valuation theoretic and model theoretic aspects of local uniformization in Hauser et al. Resolution of singularities p.389 ff. excerpted below. You can find full proofs in the links following the excerpt. See also Ribenboim, Equivalent forms of Hensel's lemma, Exposition. Math. 3 (1985), no. 1, 3-24.

[K2] 10.5 The multidimensional Hensel's Lemma, in Ch. 10, Hensel's Lemma, in
Draft of Franz-Viktor Kuhlmann's book on Valuation Theory.

[PZ] A. Prestel, M. Ziegler, Model-theoretic methods in the theory of topological fields.
J. Reine Angew. Math. 299(300) (1978), 318-341

Although it might not be exactly the same result, you can see both principles as a way to go from "local" solutions to "global" solutions for an equation. Here's a very rough sketch of how I think about it (in each case there are some adjustments to be made if you want a rigorous statement).

First, note that the implicit function theorem is usually formulated with a function of two variables $x$ and $y$ (it goes "for all y, there is a unique x ..."), but $y$ will be fixed throughout so I'll omit it. Start form an "approximate" solution $x$ to your equation (in the implicit theorem case, you take $(x_0, y_0)$ an actual solution, and then $(x_0, y)$ is an approximate solution). In each case, you want to solve $f(x+h) = 0$. Now when $h$ is "small", because $f$ is "sufficiently regular", you can write

$$f(x+h) = f(x) + f'(x).h +o(h)$$

So the rough idea (or guess), would be that has unique solution $f(x+h) = 0$ if $f(x) + f'(x).h = 0$ has one, which would be the case if $f'(x)$ is invertible (if $f$ is multivariate, $f'(x)$ is understood as the differential, meaning it's invertible when the Jacobian is non zero). Both theorems more or less state that it actually works.