no goals
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
⊢ IsUnit (gcd x y) ↔ IsCoprime x y
rw [IsCoprime, ← Ideal.mem_span_pair, ← span_gcd, ← span_singleton_eq_top, eq_top_iff_one]