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.

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} [NNRatCast K] :
          ℚ≥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
            Equations
            • NNRatCast.toCoeTail = { coe := NNRat.cast }
            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