no goals
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type ?u.3005121
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type ?u.3005358
inst✝ : CommRing P
m : ℤ
⊢ mk (↑m) 1 = ↑m
simpa using @mk_algebraMap R _ M ℤ _ _ m