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.

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

def NNRat : Type

Nonnegative rational numbers.

Equations

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

def «termℚ≥0» : Lean.ParserDescr

Nonnegative rational numbers.

Equations

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

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

  The canonical homomorphism ℚ≥0 → K.

  Do not use directly. Use the coercion instead.

instance NNRat.instNNRatCast : NNRatCast ℚ≥0

Equations

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

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

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

Equations

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

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

Equations

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

instance Rat.instNNRatCast : NNRatCast ℚ

Equations

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

Numerator and denominator of a nonnegative rational

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

The numerator of a nonnegative rational.

Equations

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

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

The denominator of a nonnegative rational.

Equations

• q.den = (↑q).den

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