abs_eq_iff_mul_self_eq — Mathlib

English

Two numbers have equal absolute values if and only if their squares are equal: |a| = |b| ⇔ a^2 = b^2.

Русский

Два числа имеют одинаковые модуль, если и только если их квадраты равны: |a| = |b| ⇔ a^2 = b^2.

LaTeX

$$$|a| = |b| \iff a^{2} = b^{2}$$$

Lean4

theorem abs_eq_iff_mul_self_eq : |a| = |b| ↔ a * a = b * b :=
  by
  rw [← abs_mul_abs_self, ← abs_mul_abs_self b]
  exact (mul_self_inj (abs_nonneg a) (abs_nonneg b)).symm

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