Documentation

Std.Data.Rat.Basic

Basics for the Rational Numbers #

theorem Rat.ext_iff (x : Rat) (y : Rat) :
x = y x.num = y.num x.den = y.den
theorem Rat.ext (x : Rat) (y : Rat) (num : x.num = y.num) (den : x.den = y.den) :
x = y
structure Rat :
  • mk' :: (
    • num : Int

      The numerator of the rational number is an integer.

    • den : Nat

      The denominator of the rational number is a natural number.

    • den_nz : s.den 0

      The denominator is nonzero.

    • reduced : Nat.Coprime (Int.natAbs s.num) s.den

      The numerator and denominator are coprime: it is in "reduced form".

  • )

Rational numbers, implemented as a pair of integers num / den such that the denominator is positive and the numerator and denominator are coprime.

Instances For
    theorem Rat.den_pos (self : Rat) :
    0 < self.den
    @[inline]
    def Rat.maybeNormalize (num : Int) (den : Nat) (g : Nat) (den_nz : den / g 0) (reduced : Nat.Coprime (Int.natAbs (Int.div num g)) (den / g)) :

    Auxiliary definition for Rat.normalize. Constructs num / den as a rational number, dividing both num and den by g (which is the gcd of the two) if it is not 1.

    Instances For
      theorem Rat.normalize.den_nz {num : Int} {den : Nat} {g : Nat} (den_nz : den 0) (e : g = Nat.gcd (Int.natAbs num) den) :
      den / g 0
      theorem Rat.normalize.reduced {num : Int} {den : Nat} {g : Nat} (den_nz : den 0) (e : g = Nat.gcd (Int.natAbs num) den) :
      Nat.Coprime (Int.natAbs (Int.div num g)) (den / g)
      @[inline]
      def Rat.normalize (num : Int) (den : optParam Nat 1) (den_nz : autoParam (den 0) _auto✝) :

      Construct a normalized Rat from a numerator and nonzero denominator. This is a "smart constructor" that divides the numerator and denominator by the gcd to ensure that the resulting rational number is normalized.

      Instances For
        def mkRat (num : Int) (den : Nat) :

        Construct a rational number from a numerator and denominator. This is a "smart constructor" that divides the numerator and denominator by the gcd to ensure that the resulting rational number is normalized, and returns zero if den is zero.

        Instances For
          def Rat.ofInt (num : Int) :

          Embedding of Int in the rational numbers.

          Instances For
            @[inline]
            def Rat.isInt (a : Rat) :

            Is this rational number integral?

            Instances For
              def Rat.divInt :
              IntIntRat

              Form the quotient n / d where n d : Int.

              Instances For

                Form the quotient n / d where n d : Int.

                Instances For
                  @[irreducible]
                  def Rat.ofScientific (m : Nat) (s : Bool) (e : Nat) :

                  Implements "scientific notation" 123.4e-5 for rational numbers. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.ofScientific_def, Rat.ofScientific_true_def, or Rat.ofScientific_false_def instead.)

                  Instances For
                    def Rat.blt (a : Rat) (b : Rat) :

                    Rational number strictly less than relation, as a Bool.

                    Instances For
                      @[irreducible]
                      def Rat.mul (a : Rat) (b : Rat) :

                      Multiplication of rational numbers. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.mul_def instead.)

                      Instances For
                        @[irreducible]
                        def Rat.inv (a : Rat) :

                        The inverse of a rational number. Note: inv 0 = 0. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.inv_def instead.)

                        Instances For
                          def Rat.div :
                          RatRatRat

                          Division of rational numbers. Note: div a 0 = 0.

                          Instances For

                            Division of rational numbers. Note: div a 0 = 0. Written with a separate function Rat.div as a wrapper so that the definition is not unfolded at .instance transparency.

                            theorem Rat.add.aux (a : Rat) (b : Rat) {g : Nat} {ad : Nat} {bd : Nat} (hg : g = Nat.gcd a.den b.den) (had : ad = a.den / g) (hbd : bd = b.den / g) :
                            let den := ad * b.den; let num := a.num * bd + b.num * ad; Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
                            @[irreducible]
                            def Rat.add (a : Rat) (b : Rat) :

                            Addition of rational numbers. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.add_def instead.)

                            Instances For
                              def Rat.neg (a : Rat) :

                              Negation of rational numbers.

                              Instances For
                                theorem Rat.sub.aux (a : Rat) (b : Rat) {g : Nat} {ad : Nat} {bd : Nat} (hg : g = Nat.gcd a.den b.den) (had : ad = a.den / g) (hbd : bd = b.den / g) :
                                let den := ad * b.den; let num := a.num * bd - b.num * ad; Nat.gcd (Int.natAbs num) g = Nat.gcd (Int.natAbs num) den
                                @[irreducible]
                                def Rat.sub (a : Rat) (b : Rat) :

                                Subtraction of rational numbers. (This definition is @[irreducible] because you don't want to unfold it. Use Rat.sub_def instead.)

                                Instances For
                                  def Rat.floor (a : Rat) :

                                  The floor of a rational number a is the largest integer less than or equal to a.

                                  Instances For
                                    def Rat.ceil (a : Rat) :

                                    The ceiling of a rational number a is the smallest integer greater than or equal to a.

                                    Instances For