no goals
α : Type ?u.296154
R : Type ?u.296157
k : Type ?u.296160
S : Type ?u.296163
M : Type u_1
M₂ : Type ?u.296169
M₃ : Type ?u.296172
ι : Type ?u.296175
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : CharZero R
v : M
⊢ v = -v ↔ v = 0
rw [← two_nsmul_eq_zero R M, two_smul, add_eq_zero_iff_eq_neg]