no goals
R : Type ?u.150711
inst✝⁹ : CommRing R
M : Submonoid R
S : Type ?u.150917
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
P : Type ?u.151171
inst✝⁶ : CommRing P
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : UniqueFactorizationMonoid A
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x : K
h : num A x = 0
⊢ 0 * ↑(algebraMap (?m.152136 h) K) ↑(den (?m.152136 h) x) = ↑(algebraMap (?m.152136 h) K) (num (?m.152136 h) x)
rw [MulZeroClass.zero_mul, h, RingHom.map_zero]