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.
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
- 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] norm}
{F : polynomial ℤ_[p]}
(hnorm : filter.tendsto (λ (i : ℕ), ∥polynomial.eval (⇑ncs i) F∥) filter.at_top (𝓝 0)) :
polynomial.eval ncs.lim F = 0
theorem
hensels_lemma
{p : ℕ}
[fact (nat.prime p)]
{F : polynomial ℤ_[p]}
{a : ℤ_[p]}
(hnorm : ∥polynomial.eval a F∥ < ∥polynomial.eval a (⇑polynomial.derivative F)∥ ^ 2) :
∃ (z : ℤ_[p]), polynomial.eval z F = 0 ∧ ∥z - a∥ < ∥polynomial.eval a (⇑polynomial.derivative F)∥ ∧ ∥polynomial.eval z (⇑polynomial.derivative F)∥ = ∥polynomial.eval a (⇑polynomial.derivative F)∥ ∧ ∀ (z' : ℤ_[p]), polynomial.eval z' F = 0 → ∥z' - a∥ < ∥polynomial.eval a (⇑polynomial.derivative F)∥ → z' = z