isometryEquivComplexOfIsComplex — Mathlib

English

If the infinite place v is complex, the completion v.Completion is isometric to the complex numbers ℂ.

Русский

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

LaTeX

$$$\text{IsComplex}(v) \Rightarrow v.Completion \cong_i \mathbb{C}$$$

Lean4

/-- If the infinite place `v` is complex, then `v.Completion` is isometric to `ℂ`. -/
def isometryEquivComplexOfIsComplex {v : InfinitePlace K} (hv : IsComplex v) : v.Completion ≃ᵢ ℂ
    where
  toEquiv := ringEquivComplexOfIsComplex hv
  isometry_toFun := isometry_extensionEmbedding v

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