no goals
α : Type ?u.106759
R : Type u_1
k : Type ?u.106765
S : Type ?u.106768
M : Type u_2
M₂ : Type ?u.106774
M₃ : Type ?u.106777
ι : Type ?u.106780
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r s : R
x✝ y : M
u : Rˣ
x : M
⊢ -u • x = -(u • x)
rw [Units.smul_def, Units.val_neg, _root_.neg_smul, Units.smul_def]