Basics for the Rational Numbers

theorem Rat.ext_iff (x : Rat) (y : Rat) : x = y ↔ x.num = y.num ∧ x.den = y.den

theorem Rat.ext (x : Rat) (y : Rat) (num : x.num = y.num) (den : x.den = y.den) : x = y

structure Rat : Type

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".

• )

instance instDecidableEqRat : DecidableEq Rat

Equations

• instDecidableEqRat = decEqRat✝

instance instInhabitedRat : Inhabited Rat

Equations

• instInhabitedRat = { default := Rat.mk' 0 1 }

instance instToStringRat : ToString Rat

Equations

• One or more equations did not get rendered due to their size.

instance instReprRat : Repr Rat

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)) : Rat

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

• Rat.maybeNormalize num den g den_nz reduced = if hg : g = 1 then Rat.mk' num den else Rat.mk' (Int.div num ↑g) (den / g)

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 : optParam Nat 1) (den_nz : autoParam (den ≠ 0) _auto✝) : Rat

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

• One or more equations did not get rendered due to their size.

def mkRat (num : Int) (den : Nat) : Rat

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

• mkRat num den = if den_nz : den = 0 then Rat.mk' 0 1 else Rat.normalize num den

def Rat.ofInt (num : Int) : Rat

Embedding of Int in the rational numbers.

Equations

• Rat.ofInt num = Rat.mk' num 1

instance Rat.instIntCastRat : IntCast Rat

Equations

• Rat.instIntCastRat = { intCast := Rat.ofInt }

instance Rat.instOfNatRat {n : Nat} : OfNat Rat n

Equations

• Rat.instOfNatRat = { ofNat := ↑↑n }

@[inline]

def Rat.isInt (a : Rat) : Bool

Is this rational number integral?

Equations

• Rat.isInt a = (a.den == 1)

def Rat.divInt : Int → Int → Rat

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

Equations

• Rat.divInt x✝ x = match x✝, x with | n, Int.ofNat d => inline (mkRat n d) | n, Int.negSucc d => Rat.normalize (-n) (Nat.succ d)

def Rat.«term_/._» : Lean.TrailingParserDescr

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

Equations

• Rat.«term_/._» = Lean.ParserDescr.trailingNode `Rat.term_/._ 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " /. ") (Lean.ParserDescr.cat `term 71))

@[irreducible]

def Rat.ofScientific (m : Nat) (s : Bool) (e : Nat) : Rat

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

• Rat.ofScientific m s e = if s = true then Rat.normalize (↑m) (10 ^ e) else ↑↑(m * 10 ^ e)

instance Rat.instOfScientificRat : OfScientific Rat

Equations

• Rat.instOfScientificRat = { ofScientific := Rat.ofScientific }

def Rat.blt (a : Rat) (b : Rat) : Bool

Rational number strictly less than relation, as a Bool.

Equations

• One or more equations did not get rendered due to their size.

instance Rat.instLTRat : LT Rat

Equations

• Rat.instLTRat = { lt := fun (x x_1 : Rat) => Rat.blt x x_1 = true }

instance Rat.instDecidableLtRatInstLTRat (a : Rat) (b : Rat) : Decidable (a < b)

Equations

• Rat.instDecidableLtRatInstLTRat a b = inferInstanceAs (Decidable (Rat.blt a b = true))

instance Rat.instLERat : LE Rat

Equations

• Rat.instLERat = { le := fun (a b : Rat) => Rat.blt b a = false }

instance Rat.instDecidableLeRatInstLERat (a : Rat) (b : Rat) : Decidable (a ≤ b)

Equations

• Rat.instDecidableLeRatInstLERat a b = inferInstanceAs (Decidable (Rat.blt b a = false))

@[irreducible]

def Rat.mul (a : Rat) (b : Rat) : Rat

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

Equations

• Rat.mul a b = let g1 := Nat.gcd (Int.natAbs a.num) b.den; let g2 := Nat.gcd (Int.natAbs b.num) a.den; Rat.mk' (Int.div a.num ↑g1 * Int.div b.num ↑g2) (a.den / g2 * (b.den / g1))

instance Rat.instMulRat : Mul Rat

Equations

• Rat.instMulRat = { mul := Rat.mul }

@[irreducible]

def Rat.inv (a : Rat) : 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

• Rat.inv a = if h : a.num < 0 then Rat.mk' (-↑a.den) (Int.natAbs a.num) else if h : a.num > 0 then Rat.mk' (↑a.den) (Int.natAbs a.num) else a

def Rat.div : Rat → Rat → Rat

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

Equations

• Rat.div x✝ x = x✝ * Rat.inv x

instance Rat.instDivRat : Div Rat

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

• Rat.instDivRat = { div := Rat.div }

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) : 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.

instance Rat.instAddRat : Add Rat

Equations

• Rat.instAddRat = { add := Rat.add }

def Rat.neg (a : Rat) : Rat

Negation of rational numbers.

Equations

• Rat.neg a = Rat.mk' (-a.num) a.den

instance Rat.instNegRat : Neg Rat

Equations

• Rat.instNegRat = { neg := Rat.neg }

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) : 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.

instance Rat.instSubRat : Sub Rat

Equations

• Rat.instSubRat = { sub := Rat.sub }

def Rat.floor (a : Rat) : Int

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

Equations

• Rat.floor a = if a.den = 1 then a.num else a.num / ↑a.den

def Rat.ceil (a : Rat) : Int

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

Equations

• Rat.ceil a = if a.den = 1 then a.num else a.num / ↑a.den + 1