no goals
α : Type ?u.111911
R : Type u_2
k : Type ?u.111917
S : Type ?u.111920
M : Type u_1
M₂ : Type ?u.111926
M₃ : Type ?u.111929
ι : Type ?u.111932
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : R
x✝ y x : M
⊢ -1 • x = -x
simp