nonnegg_pos_neg

Mathlib.NumberTheory.Zsqrtd.Basic

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

English

For c,d and a,b natural numbers, Nonnegg c d a ( -b ) is equivalent to SqLe b c a d.

Русский

Для c,d и a,b ∈ ℕ, Nonnegg c d a ( -b ) эквивалентно SqLe b c a d.

LaTeX

$$$\mathrm{Nonnegg}(c,d)(a,-b) \iff \mathrm{SqLe}(b,c,a,d)$$$

Lean4

theorem nonnegg_pos_neg {c d} {a b : ℕ} : Nonnegg c d a (-b) ↔ SqLe b c a d := by rw [nonnegg_comm];
  exact nonnegg_neg_pos

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

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

Разделы

Аффилиация

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