noncomputable def ratEmbedPadicCompletion (p : ℕ) [hp : Fact (Nat.Prime p)] : ℚ →+* (Rat.padicValuation p).Completion

Canonical ring homomorphism from $\mathbb{Q}$ into the uniform-space completion with respect to the $p$-adic valuation, obtained by composing the WithVal identification with the completion's coercion ring hom.

theorem padic_withValRingEquiv_ratEmbed (p : ℕ) [hp : Fact (Nat.Prime p)] (q : ℚ) : Padic.withValRingEquiv ((ratEmbedPadicCompletion p) q) = ↑q

Compatibility: applying the canonical ring isomorphism Padic.withValRingEquiv to the image of a rational number $q$ under ratEmbedPadicCompletion recovers the usual coercion of $q$ into $\mathbb{Q}_p$.

theorem thm_8_1_padic_completion (p : ℕ) [hp : Fact (Nat.Prime p)] : ∃ (π : (Rat.padicValuation p).Completion ≃+* ℚ_[p]), ∀ (q : ℚ), ‖π ((ratEmbedPadicCompletion p) q)‖ = ↑(padicNorm p q)

Theorem 8.1: there is a ring isomorphism between the uniform-space completion of $\mathbb{Q}$ under the $p$-adic valuation and Mathlib's $\mathbb{Q}_p$, which is an isometry on the image of $\mathbb{Q}$, i.e. the norm of $\pi(q)$ equals $|q|_p$ for every rational $q$.

noncomputable def padic_completion_ringEquiv (p : ℕ) [hp : Fact (Nat.Prime p)] : (Rat.padicValuation p).Completion ≃+* ℚ_[p]

Ring isomorphism between the uniform completion of $\mathbb{Q}$ under the $p$-adic valuation and Mathlib's $\mathbb{Q}_p$.

noncomputable def padic_completion_uniformEquiv (p : ℕ) [hp : Fact (Nat.Prime p)] : (Rat.padicValuation p).Completion ≃ᵤ ℚ_[p]

Uniform-space isomorphism between the uniform completion of $\mathbb{Q}$ under the $p$-adic valuation and Mathlib's $\mathbb{Q}_p$, witnessing that the two completions agree as uniform spaces.