Documentation

Mathlib.Algebra.Ring.Rat

The rational numbers are a commutative ring #

This file contains the commutative ring instance on the rational numbers.

See note [foundational algebra order theory].

Instances #

source
instance Rat.commRing :
CommRing ℚ
Equations
    source
    instance Rat.commGroupWithZero :
    CommGroupWithZero ℚ
    Equations
      source
      instance Rat.isDomain :
      IsDomain ℚ
      source
      instance Rat.instCharZero :
      CharZero ℚ

      The characteristic of ℚ is 0.

      Stacks Tag 09FS (Second part.)

      Extra instances to short-circuit type class resolution #

      These also prevent non-computable instances being used to construct these instances non-computably.

      source
      instance Rat.commSemiring :
      CommSemiring ℚ
      Equations
        source
        instance Rat.semiring :
        Semiring ℚ
        Equations

          Miscellaneous lemmas #

          source
          theorem Rat.mkRat_eq_div (n : ℤ) (d : ℕ) :
          mkRat n d = ↑n / ↑d
          source
          theorem Rat.divInt_div_divInt_cancel_left {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :
          divInt n x / divInt d x = divInt n d
          source
          theorem Rat.divInt_div_divInt_cancel_right {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :
          divInt x n / divInt x d = divInt d n
          source
          theorem Rat.num_div_den (r : ℚ) :
          ↑r.num / ↑r.den = r
          source
          @[simp]
          theorem Rat.divInt_pow (num : ℕ) (den : ℤ) (n : ℕ) :
          divInt (↑num) den ^ n = divInt (↑num ^ n) (den ^ n)
          source
          @[simp]
          theorem Rat.mkRat_pow (num den n : ℕ) :
          mkRat (↑num) den ^ n = mkRat (↑num ^ n) (den ^ n)
          source
          theorem Rat.natCast_eq_divInt (n : ℕ) :
          ↑n = divInt (↑n) 1
          source
          @[simp]
          theorem Rat.mul_den_eq_num (q : ℚ) :
          q * ↑q.den = ↑q.num
          source
          @[simp]
          theorem Rat.den_mul_eq_num (q : ℚ) :
          ↑q.den * q = ↑q.num