toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv

English

Another formulation of the equality of the two canonical equivalences described above.

Русский

Еще одно формулирование равенства двух канонических эквивалентностей, описанных выше.

LaTeX

$$$\\text{toEquiv\\_withValUniformEquiv\\_eq\\_toEquiv\\_withValRingEquiv}$$$

Lean4

@[simp]
theorem toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv :
    (withValUniformEquiv (p := p) : (Rat.padicValuation p).Completion ≃ ℚ_[p]) = (withValRingEquiv (p := p) :) :=
  rfl

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