The definition of the Rational Numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Summary #

We define a rational number q as a structure { num, denom, pos, cop }, where

num is the numerator of q,
denom is the denominator of q,
pos is a proof that denom > 0, and
cop is a proof num and denom are coprime.

Basic constructions and results are set up in data.rat.defs. As we transition to Lean 4, these two files can probably be merged again, as so much of the needed material will be in Std4 anyway.

For now, this split allows us to give the definitions of division rings and fields without significant theory imports.

The definition of the field structure on ℚ will be done in data.rat.basic once the field class has been defined.

Main Definitions #

rat is the structure encoding ℚ.

Notations #

Tags #

rat, rationals, field, ℚ, numerator, denominator, num, denom

source

structure rat :

Type

num : ℤ
denom : ℕ
pos : 0 < self.denom
cop : self.num.nat_abs.coprime self.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).

Instances for rat