GCD_with_Prime
Provedgcdprime-numbersproofwiki
Let p be a prime number. Then for all n: gcd(n, p) = p if p divides n, and 1 otherwise.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Data.Nat.GCD.Basic
Formal statement
theorem GCD_with_Prime (p n : ℕ) (hp : Nat.Prime p) : Nat.gcd n p = if p ∣ n then p else 1 := by sorry
Source