Hensel's lemma on ℤ_p #
This file proves Hensel's lemma on ℤ_p, roughly following Keith Conrad's writeup:
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 #
- [R. Y. Lewis, A formal proof of Hensel's lemma over the p-adic integers][lewis2019]
Tags #
p-adic, p adic, padic, p-adic integer
theorem
padic_polynomial_dist
{p : ℕ}
[Fact p.Prime]
(F : Polynomial ℤ_[p])
(x : ℤ_[p])
(y : ℤ_[p])
:
‖Polynomial.eval x F - Polynomial.eval y F‖ ≤ ‖x - y‖
theorem
limit_zero_of_norm_tendsto_zero
{p : ℕ}
[Fact p.Prime]
{ncs : CauSeq ℤ_[p] norm}
{F : Polynomial ℤ_[p]}
(hnorm : Filter.Tendsto (fun (i : ℕ) => ‖Polynomial.eval (↑ncs i) F‖) Filter.atTop (nhds 0))
:
Polynomial.eval ncs.lim F = 0
theorem
hensels_lemma
{p : ℕ}
[Fact p.Prime]
{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