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
  • One or more equations did not get rendered due to their size.
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