no goals
β : Type ?u.296855
A : Type ?u.296858
G : Type ?u.296861
M : Type u_1
R : Type u_2
inst✝³ : Ring R
inst✝² : Monoid M
inst✝¹ : LinearOrder M
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
f : R →* M
x : R
⊢ ↑f (-x) = ↑f x
rw [← neg_one_mul, map_mul, map_neg_one, one_mul]