Std.Data.Rat.Basic

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

source

instance instDecidableEqRat :

DecidableEq Rat

Equations

instDecidableEqRat = decEqRat✝

source

instance instInhabitedRat :

Inhabited Rat

Equations

instInhabitedRat = { default := { num := 0, den := 1, den_nz := instInhabitedRat.proof_1, reduced := instInhabitedRat.proof_2 } }

source

instance instToStringRat :

ToString Rat

Equations

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

source

instance instReprRat :

Repr Rat

Equations

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

source

theorem Rat.den_pos (self : Rat) :

0 < self.den

source

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

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

source

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

source

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)

source

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

Rat.normalize num den den_nz = Rat.maybeNormalize num den (Nat.gcd (Int.natAbs num) den) ⋯ ⋯

source

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 { num := 0, den := 1, den_nz := mkRat.proof_1, reduced := mkRat.proof_2 } else Rat.normalize num den den_nz

source

def Rat.ofInt (num : Int) :

Rat

Embedding of Int in the rational numbers.

Equations

Rat.ofInt num = { num := num, den := 1, den_nz := Rat.ofInt.proof_1, reduced := ⋯ }

source

instance Rat.instNatCastRat :

NatCast Rat

Equations

Rat.instNatCastRat = { natCast := fun (n : Nat) => Rat.ofInt ↑n }

source

instance Rat.instIntCastRat :

IntCast Rat

Equations

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

source

instance Rat.instOfNatRat {n : Nat} :

OfNat Rat n

Equations

Rat.instOfNatRat = { ofNat := ↑n }

source

@[inline]

def Rat.isInt (a : Rat) :

Bool

Is this rational number integral?

Equations

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

source

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) ⋯

source

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

source

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

source

instance Rat.instOfScientificRat :

OfScientific Rat

Equations

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

source

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.

source

instance Rat.instLTRat :

LT Rat

Equations

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

source

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

Decidable (a < b)

Equations

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

source

instance Rat.instLERat :

LE Rat

Equations

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

source

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

Decidable (a ≤ b)

Equations

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

source

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

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

source

instance Rat.instMulRat :

Mul Rat

Equations

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

source

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

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

source

def Rat.div :

Rat → Rat → Rat

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

Equations

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

source

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 }

source

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

source

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

source

instance Rat.instAddRat :

Add Rat

Equations

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

source

def Rat.neg (a : Rat) :

Rat

Negation of rational numbers.

Equations

Rat.neg a = { num := -a.num, den := a.den, den_nz := ⋯, reduced := ⋯ }

source

instance Rat.instNegRat :

Neg Rat

Equations

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

source

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