lean_workbook_plus_45245

Proved

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

Given that the greatest common divisor of two integers a and b is 1 (i.e., $\gcd(a,b)=1$ ), prove that there exist integers x and y such that $ax+by=1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45245 (a b : ℤ) (h : Nat.gcd a.natAbs b.natAbs = 1) : ∃ x y : ℤ, a*x + b*y = 1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph