lean_workbook_plus_77806

Proved

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

If $q$ is a positive rational number, then we can write $q=\frac{m}{n}$ for some positive integers with $\gcd(m,n)=1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_77806 (q : ℚ) (q_pos : 0 < q) : ∃ m n : ℤ, q = m / n ∧ Int.gcd m n = 1   :=  by sorry

Source