Basic definitions around the rational numbers #

This file declares ℚ notation for the rationals and defines the nonnegative rationals ℚ≥0.

This file is eligible to upstreaming to Batteries.

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

Equations
Instances For
def NNRat :

Nonnegative rational numbers.

Equations
Instances For

Nonnegative rational numbers.

Equations
Instances For

Cast from NNRat#

This section sets up the typeclasses necessary to declare the canonical embedding ℚ≥0 to any semifield.

class NNRatCast (K : Type u_1) :
Type u_1

Typeclass for the canonical homomorphism ℚ≥0 → K.

This should be considered as a notation typeclass. The sole purpose of this typeclass is to be extended by DivisionSemiring.

• nnratCast : ℚ≥0K

The canonical homomorphism ℚ≥0 → K.

Do not use directly. Use the coercion instead.

Instances
Equations
@[reducible, match_pattern]
def NNRat.cast {K : Type u_1} [] :
ℚ≥0K

Canonical homomorphism from ℚ≥0 to a division semiring K.

This is just the bare function in order to aid in creating instances of DivisionSemiring.

Equations
• NNRat.cast = NNRatCast.nnratCast
Instances For
instance NNRatCast.toCoeTail {K : Type u_1} [] :
Equations
• NNRatCast.toCoeTail = { coe := NNRat.cast }
instance NNRatCast.toCoeHTCT {K : Type u_1} [] :
Equations
• NNRatCast.toCoeHTCT = { coe := NNRat.cast }
Equations

Numerator and denominator of a nonnegative rational #

def NNRat.num (q : ℚ≥0) :

The numerator of a nonnegative rational.

Equations
• q.num = (↑q).num.natAbs
Instances For
def NNRat.den (q : ℚ≥0) :

The denominator of a nonnegative rational.

Equations
• q.den = (↑q).den
Instances For
@[simp]
theorem NNRat.num_mk (q : ) (hq : 0 q) :
NNRat.num q, hq = q.num.natAbs
@[simp]
theorem NNRat.den_mk (q : ) (hq : 0 q) :
NNRat.den q, hq = q.den
theorem NNRat.cast_id (n : ℚ≥0) :
n = n
@[simp]
theorem NNRat.cast_eq_id :
NNRat.cast = id
theorem Rat.cast_id (n : ) :
n = n
@[simp]
theorem Rat.cast_eq_id :
Rat.cast = id