The construction of ℝ using Cauchy sequences of rationals can be generalized to any absolute
value on ℚ. For any prime p, the completion of ℚ with repsect to the p-adic norm creates a field
ℚ_p and a ring ℤ_p.
padic_norm.lean defines the p-adic valuation ℤ → ℕ, extends it to ℚ, and defines
padic_norm {p} : prime p → ℚ → ℚ. Note that this does not lead to a useful instance of
has_norm since p cannot be inferred from the input, and it is not a norm for
composite p. padic_norm is shown to be a non-archimedean absolute value.p and [fact p.prime]. padic_rationals.lean defines ℚ_[p] as the Cauchy completion of
ℚ wrt padic_norm p using the same mechanisms as data/real/basic.lean. It is immediately a
field. The norm lifts to padic_norm_e : ℚ_[p] → ℚ, which is cast to ℝ and gives us a
normed_field instance. ℚ_[p] is shown to be Cauchy complete.padic_integers.lean defines ℤ_[p] as the subtype {x : ℚ_[p] \\ ∥x∥ ≤ 1}. It instantiates
local_ring and normed_ring and is Cauchy complete.hensel.lean proves Hensel's lemma over ℤ_[p], described by Gouvêa (1997) as the "most
important algebraic property of the p-adic numbers." For F : polynomial ℤ_[p] and a : ℤ_[p]
with ∥F.eval a∥ < ∥F.derivative.eval a∥^2, then there exists a unique z such that
F.eval z = 0 ∧ ∥z - a∥ < ∥F.derivative.eval a∥; furthermore,
∥F.derivative.eval z∥ = ∥F.derivative.eval a∥. The proof is an adaptation of
a writeup by Keith Conrad and
uses Newton's method to construct a sequence in ℤ_[p] converging to the unique solution.