Not_Coprime_means_Common_Prime_Factor
Provedcoprime-integersprime-numbersproofwiki
If d > 1 divides both a and b, then a and b have a common prime divisor.
Preamble
import Mathlib.RingTheory.Int.Basic
Formal statement
theorem Not_Coprime_means_Common_Prime_Factor (a b : ℤ) (d : ℤ) (hd : 1 < d) (hda : d ∣ a) (hdb : d ∣ b) : ∃ p : ℤ, Prime p ∧ p ∣ a ∧ p ∣ b := by sorry
Source