ofReal — Mathlib

English

The coercion of Real into K (RCLike field) satisfies (x : K) = Algebra.cast x, i.e., the real embedding is the algebra map.

Русский

Встраивание действительных чисел в поле RCLike равняется отображению через каноническую алгебраическую вложенность; (x : K) = Algebra.cast x.

LaTeX

$$$\operatorname{ofReal} = \mathrm{algebraMap}_{\mathbb{R},K}$$$

Lean4

/-- Coercion from `ℝ` to an `RCLike` field. -/
@[coe]
abbrev ofReal : ℝ → K :=
  Algebra.cast

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