natAbs_le_self_sq

Mathlib.Algebra.Order.Group.Unbundled.Int

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

English

For any integer a, |a| ≤ a^2.

Русский

Для любого целого a верно |a| ≤ a^2.

LaTeX

$$$ |a| \le a^2. $$$

Lean4

theorem natAbs_le_self_sq (a : ℤ) : (Int.natAbs a : ℤ) ≤ a ^ 2 :=
  by
  rw [← Int.natAbs_sq a, sq]
  norm_cast
  apply Nat.le_mul_self

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

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

Разделы

Аффилиация

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