Documentation

@[implicit_reducible]

instance Rat.commRing :

CommRing ℚ

@[implicit_reducible]

instance Rat.commGroupWithZero :

CommGroupWithZero ℚ

instance Rat.isDomain :

IsDomain ℚ

instance Rat.instCharZero :

CharZero ℚ

The characteristic of ℚ is 0.

Extra instances to short-circuit type class resolution #

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

@[implicit_reducible]

instance Rat.commSemiring :

CommSemiring ℚ

@[implicit_reducible]

instance Rat.semiring :

Semiring ℚ

Miscellaneous lemmas #

theorem Rat.divInt_div_divInt_cancel_left {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :

divInt n x / divInt d x = divInt n d

theorem Rat.divInt_div_divInt_cancel_right {x : ℤ} (hx : x ≠ 0) (n d : ℤ) :

divInt x n / divInt x d = divInt d n

theorem Rat.num_div_den (r : ℚ) :

↑r.num / ↑r.den = r

@[simp]

theorem Rat.divInt_pow (num : ℕ) (den : ℤ) (n : ℕ) :

divInt (↑num) den ^ n = 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 = divInt (↑n) 1

@[simp]

theorem Rat.mul_den_eq_num (q : ℚ) :

q * ↑q.den = ↑q.num