ringEquivComplexOfIsComplex — Mathlib

English

If the infinite place v of a field K is complex, then the completion v.Completion is ring-isomorphic to the complex numbers ℂ, via the natural bijection given by extending the complex embedding.

Русский

Если бесконечнаяPlacement v поля K является комплексной, то завершение v.Completion изоморфно кольцам к множеству комплексных чисел ℂ, через естественную биекцию, получаемую из продолжения вложения в ℂ.

LaTeX

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

Lean4

/-- The ring isomorphism `v.Completion ≃+* ℂ`, when `v` is complex, given by the bijection
`v.Completion →+* ℂ`. -/
def ringEquivComplexOfIsComplex {v : InfinitePlace K} (hv : IsComplex v) : v.Completion ≃+* ℂ :=
  RingEquiv.ofBijective _ (bijective_extensionEmbedding_of_isComplex hv)

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