isometry_extensionEmbeddingOfIsReal

English

If v is complex, the extensionEmbedding is surjective onto ℂ.

Русский

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

LaTeX

$$Function.Surjective (extensionEmbedding v)$$

Lean4

/-- The embedding `v.Completion →+* ℝ` at a real infinite place is an isometry. -/
theorem isometry_extensionEmbeddingOfIsReal {v : InfinitePlace K} (hv : IsReal v) :
    Isometry (extensionEmbeddingOfIsReal hv) :=
  Isometry.of_dist_eq (extensionEmbedding_dist_eq_of_comp <| v.norm_embedding_of_isReal hv)

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