Hensel's lemma

Stream: Is there code for X?

[Alex Zhao]

is there code for hensel's lemma?

[Thomas Browning]

https://github.com/leanprover-community/mathlib/search?q=hensel

[Thomas Browning]

Looks like mathlib might just have the p-adic version

[Kevin Buzzard]

This could be a nice project. I would imagine that some form of Hensel's lemma is true for a field equipped with a multiplicative valuation to a totally ordered monoid with zero=bot and such that the resulting topology on the field makes it complete. Then you have some integer ring, namely the stuff with valuation at most 1, and if you have a polynomial f(X) with coefficients in this integer ring and a root t satisfying $|f'(t)|<|f(t)|^2$ then the usual iterative procedure will give a sequence of elements of the field and the crucial thing will be to show that their limit is a root. If the valuation monoid is isomorphic to a subset of the reals then this works and I suspect it won't work in general so probably the general version is for "rank 1 fields"? Maybe we need a theory of commutive (semi)rings equipped with a rank one valuation -- I believe there are several equivalent conditions. How does this sound, other people who know about Hensel's Lemma?

[Adam Topaz]

I think henselian_ring could be a class. The question is what should the definition be, and in what level of generality? Note that henselianity can be defined for any pair $(A,I)$ where $A$ is a commutative ring and $I$ is an ideal of $A$.