coe_embedding_apply — Mathlib

English

For a real embedding hφ, the real-valued embedding hφ.embedding, when viewed as a complex-valued function, coincides with φ on all elements: (hφ.embedding x : ℂ) = φ(x) for all x.

Русский

Для реального вложения hφ сопоставление hφ.embedding, рассматриваемое как функция с комплексным значением, совпадает с φ на всех элементах: (hφ.embedding x : ℂ) = φ(x) для всех x.

LaTeX

$$$(h_{\\varphi}.embedding\ x : \mathbb{C}) = φ(x) \quad\text{для всех } x$$$

Lean4

@[simp]
theorem coe_embedding_apply {φ : K →+* ℂ} (hφ : IsReal φ) (x : K) : (hφ.embedding x : ℂ) = φ x :=
  by
  apply Complex.ext
  · rfl
  · rw [ofReal_im, eq_comm, ← Complex.conj_eq_iff_im]
    exact RingHom.congr_fun hφ x

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