lean_workbook_plus_16528

Proved

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

Let $a,b,c,d \in \mathbb{Z}$ such that $ad-bc\neq 0$ . Given that $ad-bc|b_1$ and $ad-bc|b_2$ , prove that there exist integers $x$ and $y$ that simultaneously satisfy $ax+by=b_1$ and $cx+dy=b_2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16528 {a b c d b1 b2 : ℤ} (h : a * d - b * c ≠ 0) (h1 : a * d - b * c ∣ b1) (h2 : a * d - b * c ∣ b2) : ∃ x y, a * x + b * y = b1 ∧ c * x + d * y = b2   :=  by sorry

Source

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

View graph