natAbs_lt_iff_mul_self_lt

Mathlib.Data.Int.Order.Lemmas

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

← MathLib Explorer

English

For all a,b ∈ ℤ, inst_LTNat.lt a.natAbs b.natAbs is equivalent to a*a < b*b.

Русский

Для всех a,b ∈ ℤ: a.natAbs < b.natAbs эквивалентно a^2 < b^2.

LaTeX

$$$\forall a,b \in \mathbb{Z}, a.\mathrm{natAbs} < b.\mathrm{natAbs} \iff a^2 < b^2.$$$

Lean4

theorem natAbs_lt_iff_mul_self_lt {a b : ℤ} : a.natAbs < b.natAbs ↔ a * a < b * b :=
  by
  rw [← abs_lt_iff_mul_self_lt, abs_eq_natAbs, abs_eq_natAbs]
  exact Int.ofNat_lt.symm

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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