English
The two canonical equivalences between the p-adic completion and Padic.p are the same when viewed as Equivalences.
Русский
Два канонических эквивалентных отображения между p-адикальным завершением и Padic равны как эквивалентности.
LaTeX
$$$\\text{toEquiv\\_withValUniformEquiv\\_eq\\_toEquiv\\_withValRingEquiv} : (\\text{withValUniformEquiv}) = (\\text{withValRingEquiv})$$$
Lean4
/-- The `p`-adic numbers are isomophic as uniform spaces to the completion of the rationals at
the `p`-adic valuation. -/
noncomputable def withValUniformEquiv : (Rat.padicValuation p).Completion ≃ᵤ ℚ_[p] :=
UniformEquiv.symm <|
Padic.withValRingEquiv.symm.toUniformEquivOfIsUniformInducing <|
isDenseInducing_cast_withVal.isUniformInducing_extend isUniformInducing_cast_withVal
(Completion.isUniformInducing_coe _)
