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)]
{R : Type u_1}
[CommSemiring R]
[Algebra R ℤ_[p]]
(F : Polynomial R)
(x y : ℤ_[p])
:
theorem
limit_zero_of_norm_tendsto_zero
{p : ℕ}
[Fact (Nat.Prime p)]
{R : Type u_1}
[CommSemiring R]
[Algebra R ℤ_[p]]
{ncs : CauSeq ℤ_[p] norm}
{F : Polynomial R}
(hnorm : Filter.Tendsto (fun (i : ℕ) => ‖(Polynomial.aeval (↑ncs i)) F‖) Filter.atTop (nhds 0))
:
theorem
hensels_lemma
{p : ℕ}
[Fact (Nat.Prime p)]
{R : Type u_1}
[CommSemiring R]
[Algebra R ℤ_[p]]
{F : Polynomial R}
{a : ℤ_[p]}
(hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2)
:
∃ (z : ℤ_[p]),
(Polynomial.aeval z) F = 0 ∧ ‖z - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ∧ ‖(Polynomial.aeval z) (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ∧ ∀ (z' : ℤ_[p]),
(Polynomial.aeval z') F = 0 → ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ → z' = z