instIsStrictOrderedRing

Mathlib.SetTheory.Surreal.Multiplication

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

English

The surreal numbers form a strict ordered ring.

Русский

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

LaTeX

$$$$ \text{Surreal is a strict ordered ring.} $$$$

Lean4

instance : IsStrictOrderedRing Surreal :=
  .of_mul_pos <| by rintro ⟨x⟩ ⟨y⟩; exact x.2.mul_pos y.2

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

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

Разделы

Аффилиация

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