sq_eq_sq_iff_abs_eq_abs

Mathlib.Algebra.Order.Ring.Abs

URI: https://scilib.ai/kg/mathlib#sq_eq_sq_iff_abs_eq_abs

English

For any a, b, a^2 = b^2 iff |a| = |b|.

Русский

Для любых a, b: a^2 = b^2 эквивалентно |a| = |b|.

LaTeX

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

Lean4

theorem sq_eq_sq_iff_abs_eq_abs (a b : α) : a ^ 2 = b ^ 2 ↔ |a| = |b| := by simp only [le_antisymm_iff, sq_le_sq]

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

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

Разделы

Аффилиация

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