HepLean 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 ℚ
Equations
source
instance Rat.instCharZero :
CharZero ℚ

The characteristic of ℚ is 0.

Stacks Tag 09FS (Second part.)

Equations

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 : ℤ) :
Rat.divInt n x / Rat.divInt d x = Rat.divInt n d
source
theorem Rat.divInt_div_divInt_cancel_right {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :
Rat.divInt x n / Rat.divInt x d = Rat.divInt d n
source
theorem Rat.num_div_den (r : ℚ) :
↑r.num / ↑r.den = r
source
@[simp]
theorem Rat.divInt_pow (num : ℕ) (den : ℤ) (n : ℕ) :
Rat.divInt (↑num) den ^ n = Rat.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 = Rat.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
source
@[deprecated Rat.natCast_eq_divInt]
theorem Rat.coe_nat_eq_divInt (n : ℕ) :
↑n = Rat.divInt (↑n) 1

Alias of Rat.natCast_eq_divInt.