Existence_of_Greatest_Common_Divisor
Provedgreatest-common-divisorproofwiki
Let a, b be integers such that a ≠ 0 or b ≠ 0. Then the greatest common divisor of a and b exists.
Preamble
import Mathlib.Data.Int.GCD
Formal statement
theorem Existence_of_Greatest_Common_Divisor (a b : ℤ) (h : a ≠ 0 ∨ b ≠ 0) : ∃ d : ℤ, d > 0 ∧ d ∣ a ∧ d ∣ b ∧ ∀ c : ℤ, c ∣ a → c ∣ b → c ∣ d := by sorry
Source