Prime_not_Divisor_implies_Coprime
Provedcoprime-integersprime-numbersproofwiki
If p is prime and p does not divide a, then p and a are coprime.
Preamble
import Mathlib.RingTheory.Int.Basic
Formal statement
theorem Prime_not_Divisor_implies_Coprime (p a : ℤ) (hp : Prime p) (hpa : ¬(p ∣ a)) : IsCoprime p a := by sorry
Source