le_total

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

There exists a total order on Z√d extending the natural order on coordinates.

Русский

Существует полный порядок на Z√d, который расширяет естественный порядок по координатам.

LaTeX

$$Le_total on Zsqrtd$$

Lean4

protected theorem le_total (a b : ℤ√d) : a ≤ b ∨ b ≤ a :=
  by
  have t := (b - a).nonneg_total
  rwa [neg_sub] at t

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

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

Разделы

Аффилиация

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