lean_workbook_plus_35816

Proved

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

Prove that, between positive integers $a$ and $b$ , $gcd(a,b)=1$ ; that is, $a$ and $b$ are relatively prime, if and only if there exist integers $x$ and $y$ such that $ax+by=1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35816 (a b : ℤ) : gcd a b = 1 ↔ ∃ x y : ℤ, a * x + b * y = 1   :=  by sorry

Source

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

View graph