English
Let φ: K → ℂ be a ring hom with image contained in ℝ. Then the associated real-valued embedding hφ: K → ℝ, defined by hφ(x) = Re(φ(x)), is a ring hom and satisfies (hφ.embedding x) = φ(x) for all x, when viewed as a complex number.
Русский
Пусть φ: K → ℂ — кольоровое гомоморфизм, чья образность лежит в ℝ. Тогда соответствующее действительное вложение hφ: K → ℝ, задаваемое hφ(x) = Re(φ(x)), является кольповым гомоморфизмом и выполняет (hφ.embedding x) = φ(x) для всех x (при таком же восприятии как комплексного числа).
LaTeX
$$$\forall x,\ (h_{\\varphi}.embedding\ x\;:\mathbb{C}) = φ(x)$$$
Lean4
/-- A real embedding as a ring homomorphism from `K` to `ℝ` . -/
def embedding {φ : K →+* ℂ} (hφ : IsReal φ) : K →+* ℝ
where
toFun x := (φ x).re
map_one' := by simp only [map_one, one_re]
map_mul' := by
simp only [Complex.conj_eq_iff_im.mp (RingHom.congr_fun hφ _), map_mul, mul_re, mul_zero, tsub_zero, forall_const]
map_zero' := by simp only [map_zero, zero_re]
map_add' := by simp only [map_add, add_re, forall_const]
