Hensel's lemma on ℤ_p #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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] has_norm.norm}
{F : polynomial ℤ_[p]}
(hnorm : 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]}
(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