no goals
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = 0
⊢ a = 0 ∧ b = 0
simpa [h] using gcd_dvd a b
case intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
⊢ gcd 0 0 = 0
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = 0 ∧ b = 0 → gcd a b = 0
rintro ⟨rfl, rfl⟩
no goals
case intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
⊢ gcd 0 0 = 0
exact gcd_zero_right _