lean_workbook_plus_34064

Proved

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

Claim: Let $a,b,c$ be positive integers so that $\gcd(a,b,c)=1$ . Then there is an integer $k$ so that $\gcd(a, b+kc)=1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34064 {a b c : ℤ} (habc : a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0) (hab : a.gcd b = 1) (hbc : a.gcd c = 1) (hca : b.gcd c = 1) : ∃ k : ℤ, a.gcd (b + k * c) = 1   :=  by sorry

Source

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

View graph