lean_workbook_plus_14189

Proved

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

Given that $k|2a$ and $k|2b$ , and $gcd(a,b)=1$ , prove that $k=1$ or $2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14189 (k a b : ℕ) (h1 : k ∣ 2 * a) (h2 : k ∣ 2 * b) (h3 : Nat.gcd a b = 1) : k = 1 ∨ k = 2   :=  by sorry

Source