instIsStrictOrderedRing

Mathlib.Analysis.Real.Hyperreal

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

English

The hyperreal numbers ℝ* form a strictly ordered ring.

Русский

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

LaTeX

$$$\mathbb{R}^* \text{ is a strictly ordered ring}$$$

Lean4

instance : IsStrictOrderedRing ℝ* :=
  inferInstanceAs (IsStrictOrderedRing (Germ _ _))

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

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

Разделы

Аффилиация

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