lean_workbook_plus_16464

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that if $d = gcd(a, b)$ , then there exist integers $x$ and $y$ such that $d = ax+by$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16464 (a b d : ℤ) (hd : d = gcd a b) : ∃ x y : ℤ, d = a * x + b * y   :=  by sorry

Source