no goals
R : Type u_1
inst✝¹³ : Ring R
R₂ : Type u_2
inst✝¹² : Ring R₂
R₃ : Type ?u.715179
inst✝¹¹ : Ring R₃
M : Type u_3
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : AddCommGroup M
M₂ : Type u_4
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : AddCommGroup M₂
M₃ : Type ?u.715203
inst✝⁶ : TopologicalSpace M₃
inst✝⁵ : AddCommGroup M₃
M₄ : Type ?u.715212
inst✝⁴ : TopologicalSpace M₄
inst✝³ : AddCommGroup M₄
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
f : M →SL[σ₁₂] M₂
x : M
⊢ ↑f (-x) = -↑f x
exact map_neg f x