no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
⊢ IsCoprime (map f p) (map f q) ↔ IsCoprime p q
rw [← EuclideanDomain.gcd_isUnit_iff, ← EuclideanDomain.gcd_isUnit_iff, gcd_map, isUnit_map]