Basics for the Rational Numbers

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 : self.num.natAbs.Coprime self.den

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

• )

@[implicit_reducible]

instance instDecidableEqRat : DecidableEq Rat

def instDecidableEqRat.decEq (x✝ x✝¹ : Rat) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance instHashableRat : Hashable Rat

def instHashableRat.hash : Rat → UInt64

@[implicit_reducible]

instance instInhabitedRat : Inhabited Rat

@[implicit_reducible]

instance instToStringRat : ToString Rat

@[implicit_reducible]

instance instReprRat : Repr Rat

theorem Rat.den_pos (self : Rat) : 0 < self.den

@[inline]

def Rat.maybeNormalize (num : Int) (den g : Nat) (dvd_num : ↑g ∣ num) (dvd_den : g ∣ den) (den_nz : den / g ≠ 0) (reduced : (num / ↑g).natAbs.Coprime (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.

theorem Rat.normalize.dvd_num {num : Int} {den g : Nat} (e : g = num.natAbs.gcd den) : ↑g ∣ num

theorem Rat.normalize.dvd_den {num : Int} {den g : Nat} (e : g = num.natAbs.gcd den) : g ∣ den

theorem Rat.normalize.den_nz {num : Int} {den g : Nat} (den_nz : den ≠ 0) (e : g = num.natAbs.gcd den) : den / g ≠ 0

theorem Rat.normalize.reduced {num : Int} {den g : Nat} (den_nz : den ≠ 0) (e : g = num.natAbs.gcd den) : (num / ↑g).natAbs.Coprime (den / g)

@[inline]

def Rat.normalize (num : Int) (den : Nat := 1) (den_nz : den ≠ 0 := by decide) : 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.

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.

def Rat.ofInt (num : Int) : Rat

Embedding of Int in the rational numbers.

@[implicit_reducible]

instance Rat.instNatCast : NatCast Rat

@[implicit_reducible]

instance Rat.instIntCast : IntCast Rat

@[implicit_reducible]

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

@[inline]

def Rat.isInt (a : Rat) : Bool

Is this rational number integral?

def Rat.divInt : Int → Int → Rat

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

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

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

@[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.)

@[implicit_reducible]

instance Rat.instOfScientific : OfScientific Rat

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

Rational number strictly less than relation, as a Bool.

@[implicit_reducible]

instance Rat.instLT : LT Rat

@[implicit_reducible]

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

@[implicit_reducible]

instance Rat.instLE : LE Rat

@[implicit_reducible]

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

@[implicit_reducible]

instance Rat.instMin : Min Rat

@[implicit_reducible]

instance Rat.instMax : Max Rat

@[irreducible]

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

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

@[implicit_reducible]

instance Rat.instMul : Mul Rat

@[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.)

@[implicit_reducible]

instance Rat.instInv : Inv Rat

def Rat.pow (q : Rat) (n : Nat) : Rat

@[implicit_reducible]

instance Rat.instPowNat : Pow Rat Nat

def Rat.zpow (q : Rat) (i : Int) : Rat

@[implicit_reducible]

instance Rat.instPowInt : Pow Rat Int

def Rat.div : Rat → Rat → Rat

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

@[implicit_reducible]

instance Rat.instDiv : 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.

theorem Rat.add.aux (a b : Rat) {g ad bd : Nat} (hg : g = a.den.gcd b.den) (had : ad = a.den / g) (hbd : bd = b.den / g) : have den := ad * b.den; have num := a.num * ↑bd + b.num * ↑ad; num.natAbs.gcd g = num.natAbs.gcd den

@[irreducible]

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

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

@[implicit_reducible]

instance Rat.instAdd : Add Rat

def Rat.neg (a : Rat) : Rat

Negation of rational numbers.

@[implicit_reducible]

instance Rat.instNeg : Neg Rat

theorem Rat.sub.aux (a b : Rat) {g ad bd : Nat} (hg : g = a.den.gcd b.den) (had : ad = a.den / g) (hbd : bd = b.den / g) : have den := ad * b.den; have num := a.num * ↑bd - b.num * ↑ad; num.natAbs.gcd g = num.natAbs.gcd den

@[irreducible]

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

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

@[implicit_reducible]

instance Rat.instSub : Sub Rat

def Rat.floor (a : Rat) : Int

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

def Rat.ceil (a : Rat) : Int

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

def Rat.abs (a : Rat) : Rat

The absolute value of a rational number a is a if a ≥ 0 and -a if a ≤ 0.