# Basics for the Rational Numbers #

structure Rat :

Rational numbers, implemented as a pair of integers num / den such that the denominator is positive and the numerator and denominator are coprime.

• mk' :: (
• num : Int

The numerator of the rational number is an integer.

• den : Nat

The denominator of the rational number is a natural number.

• den_nz : self.den 0

The denominator is nonzero.

• reduced : Nat.Coprime (Int.natAbs self.num) self.den

The numerator and denominator are coprime: it is in "reduced form".

• )
Instances For
Equations
instance instInhabitedRat :
Equations
instance instToStringRat :
Equations
• One or more equations did not get rendered due to their size.
instance instReprRat :
Equations
• One or more equations did not get rendered due to their size.
theorem Rat.den_pos (self : Rat) :
0 < self.den
@[inline]
def Rat.maybeNormalize (num : Int) (den : Nat) (g : Nat) (den_nz : den / g 0) (reduced : Nat.Coprime (Int.natAbs (Int.div num g)) (den / g)) :

Auxiliary definition for Rat.normalize. Constructs num / den as a rational number, dividing both num and den by g (which is the gcd of the two) if it is not 1.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Rat.normalize.den_nz {num : Int} {den : Nat} {g : Nat} (den_nz : den 0) (e : g = Nat.gcd (Int.natAbs num) den) :
den / g 0
theorem Rat.normalize.reduced {num : Int} {den : Nat} {g : Nat} (den_nz : den 0) (e : g = Nat.gcd (Int.natAbs num) den) :
Nat.Coprime (Int.natAbs (Int.div num g)) (den / g)
@[inline]
def Rat.normalize (num : Int) (den : ) (den_nz : autoParam (den 0) _auto✝) :

Construct a normalized Rat from a numerator and nonzero denominator. This is a "smart constructor" that divides the numerator and denominator by the gcd to ensure that the resulting rational number is normalized.

Equations
Instances For
def mkRat (num : Int) (den : Nat) :

Construct a rational number from a numerator and denominator. This is a "smart constructor" that divides the numerator and denominator by the gcd to ensure that the resulting rational number is normalized, and returns zero if den is zero.

Equations
Instances For
def Rat.ofInt (num : Int) :

Embedding of Int in the rational numbers.

Equations
Instances For
Equations
Equations
instance Rat.instOfNatRat {n : Nat} :
Equations
• Rat.instOfNatRat = { ofNat := n }
@[inline]
def Rat.isInt (a : Rat) :

Is this rational number integral?

Equations
• = (a.den == 1)
Instances For

Form the quotient n / d where n d : Int.

Equations
Instances For

Form the quotient n / d where n d : Int.

Equations
Instances For
@[irreducible]
def Rat.ofScientific (m : Nat) (s : Bool) (e : Nat) :

Implements "scientific notation" 123.4e-5 for rational numbers. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.ofScientific_def, Rat.ofScientific_true_def, or Rat.ofScientific_false_def instead.)

Equations
Instances For
def Rat.blt (a : Rat) (b : Rat) :

Rational number strictly less than relation, as a Bool.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance Rat.instLTRat :
Equations
instance Rat.instDecidableLtRatInstLTRat (a : Rat) (b : Rat) :
Decidable (a < b)
Equations
instance Rat.instLERat :
Equations
Equations
@[irreducible]
def Rat.mul (a : Rat) (b : Rat) :

Multiplication of rational numbers. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.mul_def instead.)

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance Rat.instMulRat :
Equations
@[irreducible]
def Rat.inv (a : Rat) :

The inverse of a rational number. Note: inv 0 = 0. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.inv_def instead.)

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Rat.div :

Division of rational numbers. Note: div a 0 = 0.

Equations
Instances For
instance Rat.instDivRat :

Division of rational numbers. Note: div a 0 = 0. Written with a separate function Rat.div as a wrapper so that the definition is not unfolded at .instance transparency.

Equations
theorem Rat.add.aux (a : Rat) (b : Rat) {g : Nat} {ad : Nat} {bd : Nat} (hg : g = Nat.gcd a.den b.den) (had : ad = a.den / g) (hbd : bd = b.den / g) :
let den := ad * b.den; let num := a.num * bd + b.num * ad; Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
@[irreducible]
def Rat.add (a : Rat) (b : Rat) :

Addition of rational numbers. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.add_def instead.)

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
def Rat.neg (a : Rat) :

Negation of rational numbers.

Equations
• = { num := -a.num, den := a.den, den_nz := , reduced := }
Instances For
instance Rat.instNegRat :
Equations
theorem Rat.sub.aux (a : Rat) (b : Rat) {g : Nat} {ad : Nat} {bd : Nat} (hg : g = Nat.gcd a.den b.den) (had : ad = a.den / g) (hbd : bd = b.den / g) :
let den := ad * b.den; let num := a.num * bd - b.num * ad; Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
@[irreducible]
def Rat.sub (a : Rat) (b : Rat) :

Subtraction of rational numbers. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.sub_def instead.)

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance Rat.instSubRat :
Equations
def Rat.floor (a : Rat) :

The floor of a rational number a is the largest integer less than or equal to a.

Equations
• = if a.den = 1 then a.num else a.num / a.den
Instances For
def Rat.ceil (a : Rat) :

The ceiling of a rational number a is the smallest integer greater than or equal to a.

Equations
• = if a.den = 1 then a.num else a.num / a.den + 1
Instances For