decidableLE

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

The order on Z√d is decidable: for any a,b, the statement a ≤ b is decidable.

Русский

Порядок на $\\mathbb{Z}[\\sqrt{d}]$ распознаваем: для любых $a,b$ решаемо сравнение $a \\le b$.

LaTeX

$$Decidable( a \\le b ) for all a,b ∈ \\mathbb{Z}\\sqrt{d}$$

Lean4

instance decidableLE : DecidableLE (ℤ√d) := fun _ _ => decidableNonneg _

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

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

Разделы

Аффилиация

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