eq_neg_self_iff

Mathlib.Algebra.Ring.CharZero

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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