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

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.

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

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