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