neg_units_ne_self

Mathlib.Algebra.Ring.CharZero

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

English

For every unit u in a ring R with CharZero, -u ≠ u.

Русский

Для любой единицы u в кольце R с характеристикой нуля верно, что -u ≠ u.

LaTeX

$$$-u \\neq u$$$

Lean4

@[simp]
theorem neg_units_ne_self (u : Rˣ) : -u ≠ u :=
  (units_ne_neg_self u).symm

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

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

Разделы

Аффилиация

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