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

      Nonnegative rational numbers.

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

          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
                    Instances For
                      source
                      instance NNRatCast.toCoeTail {K : Type u_1} [NNRatCast K] :
                      CoeTail ℚ≥0 K
                      Equations
                        source
                        instance NNRatCast.toCoeHTCT {K : Type u_1} [NNRatCast K] :
                        CoeHTCT ℚ≥0 K
                        Equations
                          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
                              Instances For
                                source
                                def NNRat.den (q : ℚ≥0) :
                                ℕ

                                The denominator of a nonnegative rational.

                                Equations
                                  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