We define a rational number q as a structure { num, denom, pos, cop }, where
We then define the expected (discrete) field structure on ℚ and prove basic lemmas about it. Moreoever, we provide the expected casts from ℕ and ℤ into ℚ, i.e. (↑n : ℚ) = n / 1.
rat, rationals, field, ℚ, numerator, denominator, num, denom
rat, or ℚ, is the type of rational numbers. It is defined as the set of pairs ⟨n, d⟩ of integers such that d is positive and n and d are coprime. This representation is preferred to the quotient because without periodic reduction, the numerator and denominator can grow exponentially (for example, adding 1/2 to itself repeatedly).
Embed an integer as a rational number
Form the quotient n / d where n:ℤ and d:ℕ+ (not necessarily coprime)
Form the quotient n / d where n:ℤ and d:ℕ. In the case d = 0, we define n / 0 = 0 by convention.
Form the quotient n / d where n d : ℤ.