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

source
def termℚ :
Lean.ParserDescr

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

Equations

- termℚ = Lean.ParserDescr.node `termℚ 1024 (Lean.ParserDescr.symbol "ℚ")

Instances For

source
def NNRat :
Type

Nonnegative rational numbers.

Equations

- ℚ≥0 = { q : ℚ // 0 ≤ q }

Instances For

source
def «termℚ≥0» :
Lean.ParserDescr

Nonnegative rational numbers.

Equations

- «termℚ≥0» = Lean.ParserDescr.node `«termℚ≥0» 1024 (Lean.ParserDescr.symbol "ℚ≥0")

Instances For

### Cast from `NNRat` #

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

source
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 : ℚ≥0 → K

  The canonical homomorphism `ℚ≥0 → K`.

  Do not use directly. Use the coercion instead.

Instances

source
instance NNRat.instNNRatCast :
NNRatCast ℚ≥0
Equations

- NNRat.instNNRatCast = { nnratCast := fun (q : ℚ≥0) => q }

source
@[reducible, match_pattern]
def NNRat.cast {K : Type u_1} [NNRatCast K] :
ℚ≥0 → K

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

source
instance NNRatCast.toCoeTail {K : Type u_1} [NNRatCast K] :
CoeTail ℚ≥0 K
Equations

- NNRatCast.toCoeTail = { coe := NNRat.cast }

source
instance NNRatCast.toCoeHTCT {K : Type u_1} [NNRatCast K] :
CoeHTCT ℚ≥0 K
Equations

- NNRatCast.toCoeHTCT = { coe := NNRat.cast }

source
instance Rat.instNNRatCast :
NNRatCast ℚ
Equations

- Rat.instNNRatCast = { nnratCast := Subtype.val }

### Numerator and denominator of a nonnegative rational #

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

The numerator of a nonnegative rational.

Equations

- q.num = (↑q).num.natAbs

Instances For

source
def NNRat.den (q : ℚ≥0) :
ℕ

The denominator of a nonnegative rational.

Equations

- q.den = (↑q).den

Instances For

source
@[simp]
theorem NNRat.num_mk (q : ℚ) (hq : 0 ≤ q) :
num ⟨q, hq⟩ = q.num.natAbs
source
@[simp]
theorem NNRat.den_mk (q : ℚ) (hq : 0 ≤ q) :
den ⟨q, hq⟩ = q.den
source
theorem NNRat.cast_id (n : ℚ≥0) :
↑n = n
source
@[simp]
theorem NNRat.cast_eq_id :
NNRat.cast = id
source
theorem Rat.cast_id (n : ℚ) :
↑n = n
source
@[simp]
theorem Rat.cast_eq_id :
Rat.cast = id