theorem Definition_5_1.padic_isFractionRing (p : ℕ) [Fact (Nat.Prime p)] : IsFractionRing ℤ_[p] ℚ_[p]

Definition 5.1: the field of $p$-adic numbers $\mathbb{Q}_p$ is the field of fractions of the ring of $p$-adic integers $\mathbb{Z}_p$. Witnessed by PadicInt.isFractionRing.