embedding_of_isReal_apply — Mathlib

English

For w real, and x in K, the complex value of embedding_of_isReal(hw)(x) equals embedding(w)(x).

Русский

Для реального w и элемента x ∈ K, значение в ℂ вложения embedding_of_isReal(hw)(x) равно embedding(w)(x).

LaTeX

$$$((\\mathrm{embedding\_of\_isReal} \\\\text{hw}) \\\\text{(x)} : \\\\mathbb{C}) = (\\\\mathrm{embedding}(w) \\\\text{(x)}).$$$

Lean4

@[simp]
theorem embedding_of_isReal_apply {w : InfinitePlace K} (hw : IsReal w) (x : K) :
    ((embedding_of_isReal hw) x : ℂ) = (embedding w) x :=
  ComplexEmbedding.IsReal.coe_embedding_apply (isReal_iff.mp hw) x

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