neg_sq

Mathlib.Algebra.Ring.Commute

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

English

For any a in a ring, the square of −a equals the square of a: (−a)^2 = a^2.

Русский

Для любого a в кольце квадрат −a равен квадрату a: (−a)^2 = a^2.

LaTeX

$$$ (-a)^2 = a^2 $$$

Lean4

theorem neg_sq (a : R) : (-a) ^ 2 = a ^ 2 := by simp [sq]

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

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

Разделы

Аффилиация

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