Definition_Rational_Number_Canonical_Form
Proveddefinitions-rational-numbersproofwiki
Every rational number has a canonical form p/q where p ∈ Z, q > 0, and gcd(p,q) = 1.
Preamble
import Mathlib.Data.Rat.Defs
Formal statement
theorem Definition_Rational_Number_Canonical_Form (r : ℚ) : ∃ p : ℤ, ∃ q : ℕ, 0 < q ∧ Int.gcd p q = 1 ∧ r = p / q := by sorry
Source