self_ne_neg

Mathlib.Algebra.NoZeroSMulDivisors.Basic

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

← MathLib Explorer

English

For any v in a NoZeroSMulDivisors module, v ≠ −v if and only if v ≠ 0.

Русский

Для любого v в модуле NoZeroSMulDivisors верно: v ≠ −v тогда и только тогда, когда v ≠ 0.

LaTeX

$$v \ne -v \iff v \ne 0$$

Lean4

theorem self_ne_neg (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} :
    v ≠ -v ↔ v ≠ 0 :=
  (self_eq_neg R M).not

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

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

Разделы

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

Аффилиация

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