no goals
R : Type u
inst✝¹ : CommSemiring R
x y z : R
H : IsCoprime x y
S : Type v
inst✝ : CommSemiring S
f : R →+* S
a b : R
h : a * x + b * y = 1
⊢ ↑f a * ↑f x + ↑f b * ↑f y = 1
rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]