ratCast_equiv — Mathlib

English

The canonical embedding of rationals into the completion is given by Rat.cast via the WithAbs equivalence.

Русский

Каноническое вложение рациональных чисел в дополнение задаётся через Rat.cast по эквивалентности WithAbs.

LaTeX

$$Rat.cast (WithAbs.equiv _ x) = (x : v.Completion)$$

Lean4

/-- The coercion from the rationals to its completion along an infinite place is `Rat.cast`. -/
theorem ratCast_equiv (v : InfinitePlace ℚ) (x : WithAbs v.1) : Rat.cast (WithAbs.equiv _ x) = (x : v.Completion) :=
  (eq_ratCast (UniformSpace.Completion.coeRingHom.comp (WithAbs.equiv v.1).symm.toRingHom) x).symm

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