natAbs_eq_iff_mul_self_eq

Mathlib.Data.Int.Order.Lemmas

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

← MathLib Explorer

English

For integers a,b, |a| = |b| if and only if a^2 = b^2.

Русский

Для целых a,b: |a| = |b| тогда и только тогда, когда a^2 = b^2.

LaTeX

$$$a\natextrm{natAbs} = b\natextrm{natAbs} \iff a^2 = b^2$$$

Lean4

theorem natAbs_eq_iff_mul_self_eq {a b : ℤ} : a.natAbs = b.natAbs ↔ a * a = b * b :=
  by
  rw [← abs_eq_iff_mul_self_eq, abs_eq_natAbs, abs_eq_natAbs]
  exact Int.natCast_inj.symm

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

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

Разделы

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

Аффилиация

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