extensionEmbedding — Mathlib

English

There is a natural ring embedding extensionEmbedding: v.Completion →+* ℂ.

Русский

Существует естественное вложение колец extensionEmbedding: v.Completion →+* ℂ.

LaTeX

$$extensionEmbedding : v.Completion →+* ℂ$$

Lean4

/-- The embedding associated to an infinite place extended to an embedding `v.Completion →+* ℂ`. -/
def extensionEmbedding : v.Completion →+* ℂ :=
  extensionEmbedding_of_comp v.norm_embedding_eq

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