no goals
α : Type ?u.299205
R : Type ?u.299208
k : Type ?u.299211
S : Type ?u.299214
M : Type u_1
M₂ : Type ?u.299220
M₃ : Type ?u.299223
ι : Type ?u.299226
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
v : M
⊢ -v = v ↔ v = 0
rw [eq_comm, self_eq_neg R M]