The topology of ℤ_p is the maximal-ideal-adic one

PadicInt.isAdic identifies the metric topology of ℤ_p with the adic topology of its maximal ideal pℤ_p: the ideals pⁿℤ_p are exactly the closed balls of radius p⁻ⁿ, which are open and form a neighborhood basis of 0. We register this as a Fact instance, so that ℤ_p satisfies the standing hypotheses of the p-adic kit (Chabauty.Series.PSeries).

theorem PadicInt.isAdic {p : ℕ} [hp : Fact (Nat.Prime p)] : IsAdic (IsLocalRing.maximalIdeal ℤ_[p])

The metric topology of ℤ_p is the adic topology of its maximal ideal.

instance PadicInt.instFactIsAdic {p : ℕ} [hp : Fact (Nat.Prime p)] : Fact (IsAdic (IsLocalRing.maximalIdeal ℤ_[p]))