Documentation

Mathlib.Data.Rat.Init

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
source
def NNRat :
Type

Nonnegative rational numbers.

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

Nonnegative rational numbers.

Equations

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

    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
    source
    def NNRat.den (q : ℚ≥0) :
    ℕ

    The denominator of a nonnegative rational.

    Equations
    • q.den = (↑q).den
    source
    @[simp]
    theorem NNRat.num_mk (q : ℚ) (hq : 0 ≤ q) :
    NNRat.num ⟨q, hq⟩ = q.num.natAbs
    source
    @[simp]
    theorem NNRat.den_mk (q : ℚ) (hq : 0 ≤ q) :
    NNRat.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