Elements equal to their own negative when 2 is invertible

If 2 is invertible in the scalar semiring R, then an element x of an R-module with x = -x is zero: x = ⅟2 • (x + x) = ⅟2 • (x + -x) = 0. Mathlib's self_eq_neg asks instead for the module to be additively torsion-free, which fails for instance over ZMod 3.

The same cancellation gives a scalar parity criterion: if (-1) ^ n fixes a nonzero vector, then n is even. It applies when 2 is given as a unit, without a chosen inverse.

Main results

• TauCeti.eq_zero_of_eq_neg_of_invertible_two: x = -x forces x = 0.
• TauCeti.even_of_neg_one_pow_smul_eq_self: (-1) ^ n • v = v for nonzero v forces n to be even when 2 is a unit.

theorem TauCeti.eq_zero_of_eq_neg_of_invertible_two {R : Type u_1} {M : Type u_2} [Semiring R] [Invertible 2] [AddCommGroup M] [Module R M] {x : M} (h : x = -x) : x = 0

If 2 is invertible in the scalars, an element of a module equal to its own negative is zero.

theorem TauCeti.even_of_neg_one_pow_smul_eq_self {R : Type u_1} {N : Type u_2} [Ring R] [AddCommGroup N] [Module R N] {n : ℕ} {v : N} (h2 : IsUnit 2) (hv : v ≠ 0) (h : (-1) ^ n • v = v) : Even n

If (-1) ^ n • v = v for nonzero v and a unit scalar 2, then n is even.