nonneg_iff_zero_le

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

For a ∈ Z√d with d as Nat, Nonneg a is equivalent to a ≤ 0 in the order.

Русский

Для $a \\in \\mathbb{Z}[\\sqrt{d}]$ при $d$ натуральном, Nonneg(a) эквивалентно $0 \\le a$.

LaTeX

$$Nonneg(a) ↔ 0 ≤ a$$

Lean4

theorem nonneg_iff_zero_le {a : ℤ√d} : Nonneg a ↔ 0 ≤ a :=
  show _ ↔ Nonneg _ by simp

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

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

Разделы

Аффилиация

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