embedding_of_isReal — Mathlib

English

The real embedding associated to a real infinite place hw is a real-valued embedding from K to R.

Русский

Реальное вложение, связанное с реальным бесконечным местом hw, является вложением K в ℝ, тождественным вещественному отображению.

LaTeX

$$$\\text{embedding\_of\_isReal}\\\\(hw) : K \\\\to+* \\\\mathbb{R}$$$

Lean4

/-- The real embedding associated to a real infinite place. -/
noncomputable def embedding_of_isReal {w : InfinitePlace K} (hw : IsReal w) : K →+* ℝ :=
  ComplexEmbedding.IsReal.embedding (isReal_iff.mp hw)

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