isometryEquivRealOfIsReal — Mathlib

English

If the infinite place v is real, the completion v.Completion is isometric to ℝ.

Русский

Если бесконечнаяPlacement v реален, завершение v.Completion изометрично ℝ.

LaTeX

$$$\text{IsReal}(v) \Rightarrow v.Completion \simeq_i \mathbb{R}$$$

Lean4

/-- If the infinite place `v` is real, then `v.Completion` is isometric to `ℝ`. -/
def isometryEquivRealOfIsReal {v : InfinitePlace K} (hv : IsReal v) : v.Completion ≃ᵢ ℝ
    where
  toEquiv := ringEquivRealOfIsReal hv
  isometry_toFun := isometry_extensionEmbeddingOfIsReal hv

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