no goals
α : Type ?u.55822
β : Type ?u.55825
M : Type ?u.55828
N : Type ?u.55831
P : Type ?u.55834
G : Type u_1
H : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), ↑f x⁻¹ = (↑f x)⁻¹
a : G
n : ℕ
⊢ ↑f (a ^ ↑n) = ↑f a ^ ↑n
rw [zpow_ofNat, map_pow, zpow_ofNat]
no goals
α : Type ?u.55822
β : Type ?u.55825
M : Type ?u.55828
N : Type ?u.55831
P : Type ?u.55834
G : Type u_1
H : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), ↑f x⁻¹ = (↑f x)⁻¹
a : G
n : ℕ
⊢ ↑f (a ^ Int.negSucc n) = ↑f a ^ Int.negSucc n
rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc, ← zpow_negSucc]