neg_eq'

Mathlib.Algebra.CharP.Two

URI: https://scilib.ai/kg/mathlib#CharTwo.neg_eq'

English

The negation map equals the identity map: -x = x for all x.

Русский

Группа отрицания равна тождественному отображению: -x = x для всех x.

LaTeX

$$$-x = x$$$

Lean4

theorem neg_eq' : Neg.neg = (id : R → R) :=
  funext neg_eq

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

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

Разделы

Аффилиация

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