instLECastInt

Mathlib.NumberTheory.Zsqrtd.Basic

URI: https://scilib.ai/kg/mathlib#Zsqrtd.instLECastInt

English

There is a natural order on Z√d defined by a ≤ b iff b − a is nonnegative.

Русский

Существует естественный порядок на $\\mathbb{Z}[\\sqrt{d}]$, задаваемый $a \\le b \\iff b-a \\in \\text{Nonneg}$.

LaTeX

$$$a \\le b \\iff \\operatorname{Nonneg}(b - a)$$$

Lean4

instance : LE (ℤ√d) :=
  ⟨fun a b => Nonneg (b - a)⟩

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

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

Разделы

Аффилиация

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