no goals
R : Type u_1
A : Type u_3
B : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
h : optParam (IsIntegral R 0) (_ : IsIntegral R 0)
⊢ ↑(algebraMap A B) (mk' A 0 h) = ↑(algebraMap A B) 0
rw [algebraMap_mk', RingHom.map_zero]