no goals
R : Type u_2
R₁ : Type ?u.2123585
R₂ : Type ?u.2123588
R₃ : Type ?u.2123591
R₄ : Type ?u.2123594
S : Type ?u.2123597
K : Type ?u.2123600
K₂ : Type ?u.2123603
M : Type u_1
M' : Type ?u.2123609
M₁ : Type ?u.2123612
M₂ : Type ?u.2123615
M₃ : Type ?u.2123618
M₄ : Type ?u.2123621
N : Type ?u.2123624
N₂ : Type ?u.2123627
ι : Type ?u.2123630
V : Type ?u.2123633
V₂ : Type ?u.2123636
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
⊢ ↑(neg R) x = -x
simp