Hensel's lemma on ℤ_p
This file proves Hensel's lemma on ℤ_p, roughly following Keith Conrad's writeup: http://www.math.uconn.edu/~kconrad/blurbs/gradnumthy/hensel.pdf
Hensel's lemma gives a simple condition for the existence of a root of a polynomial.
The proof and motivation are described in the paper [R. Y. Lewis, A formal proof of Hensel's lemma over the p-adic integers][lewis2019].
References
- http://www.math.uconn.edu/~kconrad/blurbs/gradnumthy/hensel.pdf
- [R. Y. Lewis, A formal proof of Hensel's lemma over the p-adic integers][lewis2019]
- https://en.wikipedia.org/wiki/Hensel%27s_lemma
Tags
p-adic, p adic, padic, p-adic integer
theorem
padic_polynomial_dist
{p : ℕ}
[fact (nat.prime p)]
(F : polynomial ℤ_[p])
(x y : ℤ_[p]) :
∥polynomial.eval x F - polynomial.eval y F∥ ≤ ∥x - y∥
theorem
limit_zero_of_norm_tendsto_zero
{p : ℕ}
[fact (nat.prime p)]
{ncs : cau_seq ℤ_[p] has_norm.norm}
{F : polynomial ℤ_[p]} :
filter.tendsto (λ (i : ℕ), ∥polynomial.eval (⇑ncs i) F∥) filter.at_top (nhds 0) → polynomial.eval ncs.lim F = 0
theorem
hensels_lemma
{p : ℕ}
[fact (nat.prime p)]
{F : polynomial ℤ_[p]}
{a : ℤ_[p]} :
∥polynomial.eval a F∥ < ∥polynomial.eval a F.derivative∥ ^ 2 → (∃ (z : ℤ_[p]), polynomial.eval z F = 0 ∧ ∥z - a∥ < ∥polynomial.eval a F.derivative∥ ∧ ∥polynomial.eval z F.derivative∥ = ∥polynomial.eval a F.derivative∥ ∧ ∀ (z' : ℤ_[p]), polynomial.eval z' F = 0 → ∥z' - a∥ < ∥polynomial.eval a F.derivative∥ → z' = z)