ofRealHom — Mathlib

English

The embedding of real numbers into complex numbers acts by sending r to r ∈ ℂ.

Русский

Встраивание вещественных чисел в комплексные действует так: r ↦ r ∈ ℂ.

LaTeX

$$$\\operatorname{ofRealHom}(r) = r$$$

Lean4

/-- The coercion `ℝ → ℂ` as a `RingHom`. -/
def ofRealHom : ℝ →+* ℂ where
  toFun x := (x : ℂ)
  map_one' := ofReal_one
  map_zero' := ofReal_zero
  map_mul' := ofReal_mul
  map_add' := ofReal_add

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