instCoeTCReal

Mathlib.Analysis.Real.Hyperreal

URI: https://scilib.ai/kg/mathlib#Hyperreal.instCoeTCReal

English

There is a canonical coercion from Real to Hyperreal numbers.

Русский

Существует каноническое приведение из Real к Hyperreal.

LaTeX

$$$\mathrm{Coercion}: \mathbb{R} \to \mathbb{R}^*$$$

Lean4

noncomputable instance : CoeTC ℝ ℝ* :=
  ⟨ofReal⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru