natAbs_eq_iff_sq_eq — Mathlib

English

For integers a and b, equality of their absolute values is equivalent to equality of their squares.

Русский

Для целых чисел a и b равенство их абсолютных значений эквивалентно равенству квадратов.

LaTeX

$$$\forall a,b \in \mathbb{Z},\ |a| = |b| \iff a^{2} = b^{2}$$$

Lean4

theorem natAbs_eq_iff_sq_eq {a b : ℤ} : a.natAbs = b.natAbs ↔ a ^ 2 = b ^ 2 :=
  by
  rw [sq, sq]
  exact natAbs_eq_iff_mul_self_eq

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