Integers_Divided_by_GCD_are_Coprime

Proved

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

coprime-integersgreatest-common-divisorproofwiki

Any pair of integers, not both zero, divided by their GCD gives a coprime pair.

Preamble

import Mathlib.Data.Int.GCD
import Mathlib.RingTheory.Int.Basic

Formal statement

theorem Integers_Divided_by_GCD_are_Coprime (a b : ℤ) (h : a ≠ 0 ∨ b ≠ 0) : IsCoprime (a / ↑(Int.gcd a b)) (b / ↑(Int.gcd a b)) := by sorry

Source