instLTCastInt

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

There is a natural strict order on Z√d defined by x < y iff not (y ≤ x).

Русский

Существует строги́й упорядочение на $\\mathbb{Z}[\\sqrt{d}]$, при котором $x < y$ если и только если не $y \\le x$.

LaTeX

$$$x < y \\iff \\lnot (y \\le x)$$$

Lean4

instance : LT (ℤ√d) :=
  ⟨fun a b => ¬b ≤ a⟩

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

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

Разделы

Аффилиация

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