ℚ_[p] is a non-archimedean local field

This file records the instance IsNonarchimedeanLocalField ℚ_[p].

instance instIsNonarchimedeanLocalFieldPadic {p : ℕ} [Fact (Nat.Prime p)] : IsNonarchimedeanLocalField ℚ_[p]

The p-adic numbers form a non-archimedean local field: the topology comes from the valuative relation, ℚ_[p] is locally compact, and the valuation is nontrivial.