instField

Mathlib.Analysis.Real.Hyperreal

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

English

The hyperreal numbers ℝ* form a field.

Русский

Гиперреальные числа ℝ* образуют поле.

LaTeX

$$$\mathbb{R}^* \text{ is a field}$$$

Lean4

noncomputable instance : Field ℝ* :=
  inferInstanceAs (Field (Germ _ _))

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

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

Разделы

Аффилиация

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