coe_withValRingEquiv_symm — Mathlib

English

The uniform equivalence between the p-adic completion and the p-adics is established by the withVal ring equivalence and its uniform extension.

Русский

Установлено единообразное эквивалентное отображение между p-адикальным завершением и p-адическими числами через соответствие withValRingEquiv и её равномерное продолжение.

LaTeX

$$${\\text{Padic.withValUniformEquiv}} : (\\text{Rat.padicValuation}(p)).Completion \\simeq_\\mu \\mathbb{Q}_p$$$

Lean4

@[simp]
theorem coe_withValRingEquiv_symm :
    ⇑(Padic.withValRingEquiv (p := p)).symm = Padic.isDenseInducing_cast_withVal.extend Completion.coe' := by rfl

Похожие утверждения