lean_workbook_plus_38388

Proved

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

Prove that if $\gcd(x,y)=d>1$ , then $d\mid x'$ and $d\mid y'$ , where $x=dx'$ and $y=dy'$ with $\gcd(x',y')=1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_38388 (x y : ℕ) (h : 1 < Nat.gcd x y) : (Nat.gcd x y) ∣ x ∧ (Nat.gcd x y) ∣ y   :=  by sorry

Source