abs_mul_abs_self

Mathlib.Algebra.Order.Ring.Abs

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

English

|a|·|a| = a·a for all a.

Русский

|a|·|a| = a·a для всех a.

LaTeX

$$$|a|\,|a| = a\,a$$$

Lean4

@[simp]
theorem abs_mul_abs_self (a : α) : |a| * |a| = a * a :=
  abs_by_cases (fun x => x * x = a * a) rfl (neg_mul_neg a a)

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

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

Разделы

Аффилиация

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