abs_sq

Mathlib.Algebra.Order.Ring.Abs

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

English

For any x, |x|^2 = x^2.

Русский

Для любого x, |x|^2 = x^2.

LaTeX

$$$|x|^{2} = x^{2}$$$

Lean4

theorem abs_sq (x : α) : |x ^ 2| = x ^ 2 := by simpa only [sq] using abs_mul_self x

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

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

Разделы

Аффилиация

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