lean_workbook_plus_77089

Proved

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

Prove that if $d = gcd(a, b)$ , then $d$ divides any linear combination of $a$ and $b$ , i.e., $d | (ax+by) \forall x, y \in \mathbb{Z}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_77089 (a b d x y : ℤ) (h₁ : d = gcd a b) : d ∣ a * x + b * y   :=  by sorry

Source