Maths in Lean : p-adic numbers #

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.