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 #

Equations
  • One or more equations did not get rendered due to their size.

Extra instances to short-circuit type class resolution #

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

Equations
Equations

Miscellaneous lemmas #

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

Alias of Rat.natCast_eq_divInt.