no goals
β : Type ?u.293119
A : Type ?u.293122
G : Type ?u.293125
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
⊢ ↑f (-1) ^ Nat.succ 1 = 1
rw [← map_pow, neg_one_sq, map_one]