sq_abs

Mathlib.Algebra.Order.Ring.Abs

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

English

The square of the absolute value equals the square of the element: |a|^2 = a^2.

Русский

Квадрат модуля равен квадрату числа: |a|^2 = a^2.

LaTeX

$$$|a|^{2} = a^{2}$$$

Lean4

@[simp]
theorem sq_abs (a : α) : |a| ^ 2 = a ^ 2 := by simpa only [sq] using abs_mul_abs_self a

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

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

Разделы

Аффилиация

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