instZeroLEOneClassCastInt

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

For the ring ℤ√d with nonsquare d, one has 0 ≤ 1 in that ordered ring.

Русский

Для кольца ℤ√d при несотиатом d выполняется 0 ≤ 1 в упорядоченном кольце.

LaTeX

$$$0 \\le 1 \\quad \\text{in } \\mathbb{Z}\\sqrt{d}, \\ d \\text{ nonsquare}.$$$

Lean4

instance : ZeroLEOneClass (ℤ√d) :=
  { zero_le_one := by trivial }

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

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

Разделы

Аффилиация

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