coe_withValRingEquiv — Mathlib

English

The coe (the underlying function) of withValRingEquiv equals the completion extension of a standard equivalence.

Русский

Собственно отображение withValRingEquiv совпадает с продолжением завершения в обычном эквиваленте.

LaTeX

$$$\\text{coe\\_withValRingEquiv} : \\big( \\text{Padic.withValRingEquiv} \\big) = \\text{Completion.extension}((\\uparrow) \\circ (WithVal.equiv (\\text{Rat.padicValuation}(p))))$$$

Lean4

@[simp]
theorem coe_withValRingEquiv :
    ⇑(Padic.withValRingEquiv (p := p)) = Completion.extension ((↑) ∘ (WithVal.equiv (Rat.padicValuation p))) :=
  rfl

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