no goals
p : ℕ
R : Type u_2
S : Type u_1
T : Type ?u.460757
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type ?u.460772
β : Type ?u.460775
f : R →+* S
x y : 𝕎 R
n : ℕ
⊢ mapFun (↑f) (x ^ n) = mapFun (↑f) x ^ n
map_fun_tac