English
For nonzero integers a and b, gcd(a,b) is the smallest positive natural number representable as a x + b y with integers x,y.
Русский
Для нес нулевых целых a и b НОД(a,b) — наименьшее положительное число, которое можно записать как a x + b y, где x,y — целые.
LaTeX
$$$$\\text{If } a\\neq 0,\\; \\gcd(a,b) \\text{ is the least } n>0 \\text{ with } \\exists x,y\\in\\mathbb{Z}, n = a x + b y.$$$$
Lean4
/-- For nonzero integers `a` and `b`, `gcd a b` is the smallest positive natural number that can be
written in the form `a * x + b * y` for some pair of integers `x` and `y` -/
theorem gcd_least_linear {a b : ℤ} (ha : a ≠ 0) : IsLeast {n : ℕ | 0 < n ∧ ∃ x y : ℤ, ↑n = a * x + b * y} (a.gcd b) :=
by
simp_rw [← gcd_dvd_iff]
constructor
· simpa [and_true, dvd_refl, Set.mem_setOf_eq] using gcd_pos_of_ne_zero_left b ha
· simp only [lowerBounds, and_imp, Set.mem_setOf_eq]
exact fun n hn_pos hn => Nat.le_of_dvd hn_pos hn
