bijective_extensionEmbedding_of_isComplex

English

If v is complex, the extensionEmbedding v is bijective.

Русский

Если место комплексное, расширяющее отображение биективно.

LaTeX

$$bijective_extensionEmbedding_of_isComplex hv$$

Lean4

/-- If `v` is a complex infinite place, then the embedding `v.Completion →+* ℂ` is bijective. -/
theorem bijective_extensionEmbedding_of_isComplex {v : InfinitePlace K} (hv : IsComplex v) :
    Function.Bijective (extensionEmbedding v) :=
  ⟨(extensionEmbedding v).injective, surjective_extensionEmbedding_of_isComplex hv⟩

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