neg_eq_self_iff

Mathlib.Algebra.Ring.CharZero

URI: https://scilib.ai/kg/mathlib#CharZero.neg_eq_self_iff

English

In a ring with NoZeroDivisors and CharZero, -a = a if and only if a = 0.

Русский

В кольце без нулевых делителей и характеристикой нуля равенство $-a = a$ имеет единственное решение $a = 0$.

LaTeX

$$$-a = a \\iff a = 0$$$

Lean4

@[scoped simp]
theorem neg_eq_self_iff {a : R} : -a = a ↔ a = 0 :=
  neg_eq_iff_add_eq_zero.trans add_self_eq_zero

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

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

Разделы

Аффилиация

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