surjective_extensionEmbedding_of_isComplex

English

If v is complex, the extensionEmbedding is surjective.

Русский

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

LaTeX

$$surjective_extensionEmbedding_of_isComplex hv$$

Lean4

/-- If `v` is a complex infinite place, then the embedding `v.Completion →+* ℂ` is surjective. -/
theorem surjective_extensionEmbedding_of_isComplex {v : InfinitePlace K} (hv : IsComplex v) :
    Function.Surjective (extensionEmbedding v) :=
  by
  rw [← RingHom.fieldRange_eq_top_iff]
  exact
    (Complex.subfield_eq_of_closed <| isClosed_image_extensionEmbedding v).resolve_left <|
      subfield_ne_real_of_isComplex hv

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