self_eq_neg — Mathlib

English

In a NoZeroSMulDivisors module over a ring of characteristic zero, the only element equal to its own negation is zero: v = −v iff v = 0.

Русский

В модуле без нулевых делителей умножения над кольцом характеристика ноль: единственный элемент, равный своему отрицанию, — ноль.

LaTeX

$$v = -v \iff v = 0$$

Lean4

theorem self_eq_neg (R) (M) [Semiring R] [CharZero R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : M} :
    v = -v ↔ v = 0 := by rw [← two_nsmul_eq_zero R M, two_smul, add_eq_zero_iff_eq_neg]

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