ofRealAm — Mathlib

English

For every real r, the real-algebra homomorphism ofRealAm sends r to the complex number r (as a real embedded into ℂ).

Русский

Для каждого действительного r отображение ofRealAm отправляет r в комплексное число r (как в ℂ через нормальное вложение).

LaTeX

$$$ \forall r \in \mathbb{R}: \mathrm{ofRealAm}(r) = r \in \mathbb{C}. $$$

Lean4

/-- `ℝ`-algebra morphism version of the canonical embedding of `ℝ` in `ℂ`. -/
def ofRealAm : ℝ →ₐ[ℝ] ℂ :=
  Algebra.ofId ℝ ℂ

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