extensionEmbeddingOfIsReal — Mathlib

English

InfinitePlace ℚ is a Subsingleton, i.e., any two infinite places are equal.

Русский

InfinitePlace(ℚ) является подподмножеством; любые два бесконечных места совпадают.

LaTeX

$$Subsingleton (InfinitePlace ℚ)$$

Lean4

/-- The embedding `K →+* ℝ` associated to a real infinite place extended to `v.Completion →+* ℝ`. -/
def extensionEmbeddingOfIsReal {v : InfinitePlace K} (hv : IsReal v) : v.Completion →+* ℝ :=
  extensionEmbedding_of_comp <| v.norm_embedding_of_isReal hv

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