sqrt_nonneg

Mathlib.Data.Int.Sqrt

URI: https://scilib.ai/kg/mathlib#Int.sqrt_nonneg

English

For every integer n, sqrt(n) is nonnegative.

Русский

Для любого целого n корень sqrt(n) неотрицателен.

LaTeX

$$$0 \le \sqrt{n}$$$

Lean4

theorem sqrt_nonneg (n : ℤ) : 0 ≤ sqrt n :=
  natCast_nonneg _

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

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

Разделы

Аффилиация

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