neg_one_sq

Mathlib.Algebra.Ring.Commute

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

English

In a ring with distributive negation, (-1)^2 = 1.

Русский

В кольце с распределимым отрицанием (-1)^2 = 1.

LaTeX

$$$ (-1)^2 = 1 $$$

Lean4

theorem neg_one_sq : (-1 : R) ^ 2 = 1 := by simp [neg_sq, one_pow]

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

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

Разделы

Аффилиация

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