units_ne_neg_self

Mathlib.Algebra.Ring.CharZero

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$u \\in R^{\\times} \\Rightarrow u \\neq -u$$$

Lean4

@[simp]
theorem units_ne_neg_self (u : Rˣ) : u ≠ -u := by
  simp_rw [ne_eq, Units.ext_iff, Units.val_neg, eq_neg_iff_add_eq_zero, ← two_mul, Units.mul_left_eq_zero, two_ne_zero,
    not_false_iff]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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