Lemmas about the Rational Numbers

theorem Rat.ext {p q : Rat} : p.num = q.num → p.den = q.den → p = q

@[simp]

theorem Rat.mk_den_one {r : Int} : { num := r, den_nz := Nat.one_ne_zero, reduced := ⋯ } = ↑r

@[simp]

theorem Rat.zero_num : num 0 = 0

@[simp]

theorem Rat.zero_den : den 0 = 1

@[simp]

theorem Rat.one_num : num 1 = 1

@[simp]

theorem Rat.one_den : den 1 = 1

@[simp]

theorem Rat.maybeNormalize_eq {num : Int} {den g : Nat} (dvd_num : ↑g ∣ num) (dvd_den : g ∣ den) (den_nz : den / g ≠ 0) (reduced : (num / ↑g).natAbs.Coprime (den / g)) : maybeNormalize num den g dvd_num dvd_den den_nz reduced = { num := num.divExact (↑g) dvd_num, den := den / g, den_nz := den_nz, reduced := reduced }

theorem Rat.normalize_eq {num : Int} {den : Nat} (den_nz : den ≠ 0) : normalize num den den_nz = { num := num / ↑(num.natAbs.gcd den), den := den / num.natAbs.gcd den, den_nz := ⋯, reduced := ⋯ }

@[simp]

theorem Rat.num_normalize {num : Int} {den : Nat} (den_nz : den ≠ 0) : (normalize num den den_nz).num = num / ↑(num.natAbs.gcd den)

@[simp]

theorem Rat.den_normalize {num : Int} {den : Nat} (den_nz : den ≠ 0) : (normalize num den den_nz).den = den / num.natAbs.gcd den

@[simp]

theorem Rat.normalize_zero {d : Nat} (nz : d ≠ 0) : normalize 0 d nz = 0

theorem Rat.mk_eq_normalize (num : Int) (den : Nat) (nz : den ≠ 0) (c : num.natAbs.Coprime den) : { num := num, den := den, den_nz := nz, reduced := c } = normalize num den nz

theorem Rat.normalize_eq_mk' (n : Int) (d : Nat) (h : d ≠ 0) (c : n.natAbs.gcd d = 1) : normalize n d h = { num := n, den := d, den_nz := h, reduced := c }

theorem Rat.normalize_self (r : Rat) : normalize r.num r.den ⋯ = r

theorem Rat.normalize_mul_left {d : Nat} {n : Int} {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0) : normalize (↑a * n) (a * d) ⋯ = normalize n d d0

theorem Rat.normalize_mul_right {d : Nat} {n : Int} {a : Nat} (d0 : d ≠ 0) (a0 : a ≠ 0) : normalize (n * ↑a) (d * a) ⋯ = normalize n d d0

theorem Rat.normalize_eq_iff {d₁ d₂ : Nat} {n₁ n₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : normalize n₁ d₁ z₁ = normalize n₂ d₂ z₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁

theorem Rat.maybeNormalize_eq_normalize {num : Int} {den g : Nat} (dvd_num : ↑g ∣ num) (dvd_den : g ∣ den) (den_nz : den / g ≠ 0) (reduced : (num / ↑g).natAbs.Coprime (den / g)) (hn : ↑g ∣ num) (hd : g ∣ den) : maybeNormalize num den g dvd_num dvd_den den_nz reduced = normalize num den ⋯

@[simp]

theorem Rat.normalize_eq_zero {d : Nat} {n : Int} (d0 : d ≠ 0) : normalize n d d0 = 0 ↔ n = 0

theorem Rat.normalize_num_den' (num : Int) (den : Nat) (nz : den ≠ 0) : ∃ (d : Nat), d ≠ 0 ∧ num = (normalize num den nz).num * ↑d ∧ den = (normalize num den nz).den * d

theorem Rat.normalize_num_den {n : Int} {d : Nat} {z : d ≠ 0} {n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : n'.natAbs.Coprime d'} (h : normalize n d z = { num := n', den := d', den_nz := z', reduced := c }) : ∃ (m : Nat), m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m

theorem Rat.normalize_eq_mkRat {num : Int} {den : Nat} (den_nz : den ≠ 0) : normalize num den den_nz = mkRat num den

theorem Rat.mkRat_num_den {d : Nat} {n n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : n'.natAbs.Coprime d'} (z : d ≠ 0) (h : mkRat n d = { num := n', den := d', den_nz := z', reduced := c }) : ∃ (m : Nat), m ≠ 0 ∧ n = n' * ↑m ∧ d = d' * m

theorem Rat.mkRat_def (n : Int) (d : Nat) : mkRat n d = if d0 : d = 0 then 0 else normalize n d d0

theorem Rat.num_mkRat (n : Int) (d : Nat) : (mkRat n d).num = if d = 0 then 0 else n / ↑(d.gcd n.natAbs)

theorem Rat.den_mkRat (n : Int) (d : Nat) : (mkRat n d).den = if d = 0 then 1 else d / d.gcd n.natAbs

@[simp]

theorem Rat.mkRat_self (a : Rat) : mkRat a.num a.den = a

theorem Rat.mk_eq_mkRat (num : Int) (den : Nat) (nz : den ≠ 0) (c : num.natAbs.Coprime den) : { num := num, den := den, den_nz := nz, reduced := c } = mkRat num den

@[simp]

theorem Rat.zero_mkRat (n : Nat) : mkRat 0 n = 0

@[simp]

theorem Rat.mkRat_zero (n : Int) : mkRat n 0 = 0

theorem Rat.mkRat_eq_zero {d : Nat} {n : Int} (d0 : d ≠ 0) : mkRat n d = 0 ↔ n = 0

theorem Rat.mkRat_ne_zero {d : Nat} {n : Int} (d0 : d ≠ 0) : mkRat n d ≠ 0 ↔ n ≠ 0

theorem Rat.mkRat_mul_left {n : Int} {d a : Nat} (a0 : a ≠ 0) : mkRat (↑a * n) (a * d) = mkRat n d

theorem Rat.mkRat_mul_right {n : Int} {d a : Nat} (a0 : a ≠ 0) : mkRat (n * ↑a) (d * a) = mkRat n d

theorem Rat.mkRat_eq_iff {d₁ d₂ : Nat} {n₁ n₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : mkRat n₁ d₁ = mkRat n₂ d₂ ↔ n₁ * ↑d₂ = n₂ * ↑d₁

@[simp]

theorem Rat.divInt_ofNat (num : Int) (den : Nat) : divInt num ↑den = mkRat num den

theorem Rat.mk_eq_divInt {num : Int} {den : Nat} {nz : den ≠ 0} {c : num.natAbs.Coprime den} : { num := num, den := den, den_nz := nz, reduced := c } = divInt num ↑den

theorem Rat.num_divInt_den (a : Rat) : divInt a.num ↑a.den = a

@[deprecated Rat.mk_eq_divInt (since := "2025-10-29")]

theorem Rat.mk'_eq_divInt {n : Int} {d : Nat} {h : d ≠ 0} {c : n.natAbs.Coprime d} : { num := n, den := d, den_nz := h, reduced := c } = divInt n ↑d

@[reducible, inline, deprecated Rat.num_divInt_den (since := "2025-08-22")]

abbrev Rat.divInt_self (a : Rat) : divInt a.num ↑a.den = a

@[simp]

theorem Rat.zero_divInt (n : Int) : divInt 0 n = 0

@[simp]

theorem Rat.divInt_zero (n : Int) : divInt n 0 = 0

theorem Rat.neg_divInt_neg (num den : Int) : divInt (-num) (-den) = divInt num den

theorem Rat.divInt_neg' (num den : Int) : divInt num (-den) = divInt (-num) den

theorem Rat.divInt_eq_divInt_iff {d₁ d₂ n₁ n₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : divInt n₁ d₁ = divInt n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

@[reducible, inline, deprecated Rat.divInt_eq_divInt_iff (since := "2025-08-22")]

abbrev Rat.divInt_eq_iff {d₁ d₂ n₁ n₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : divInt n₁ d₁ = divInt n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

theorem Rat.divInt_mul_left {n d a : Int} (a0 : a ≠ 0) : divInt (a * n) (a * d) = divInt n d

theorem Rat.divInt_mul_right {n d a : Int} (a0 : a ≠ 0) : divInt (n * a) (d * a) = divInt n d

theorem Rat.divInt_self' {n : Int} (hn : n ≠ 0) : divInt n n = 1

theorem Rat.divInt_num_den {d n n' : Int} {d' : Nat} {z' : d' ≠ 0} {c : n'.natAbs.Coprime d'} (z : d ≠ 0) (h : divInt n d = { num := n', den := d', den_nz := z', reduced := c }) : ∃ (m : Int), m ≠ 0 ∧ n = n' * m ∧ d = ↑d' * m

theorem Rat.num_divInt (a b : Int) : (divInt a b).num = b.sign * a / ↑(b.gcd a)

theorem Rat.den_divInt (a b : Int) : (divInt a b).den = if b = 0 then 1 else b.natAbs / b.gcd a

def Rat.numDenCasesOn {C : Rat → Sort u} (a : Rat) : ((n : Int) → (d : Nat) → 0 < d → n.natAbs.Coprime d → C (divInt n ↑d)) → C a

Define a (dependent) function or prove ∀ r : Rat, p r by dealing with rational numbers of the form n /. d with 0 < d and coprime n, d.

def Rat.numDenCasesOn' {C : Rat → Sort u} (a : Rat) (H : (n : Int) → (d : Nat) → d ≠ 0 → C (divInt n ↑d)) : C a

Define a (dependent) function or prove ∀ r : Rat, p r by dealing with rational numbers of the form n /. d with d ≠ 0.

def Rat.numDenCasesOn'' {C : Rat → Sort u} (a : Rat) (H : (n : Int) → (d : Nat) → (nz : d ≠ 0) → (red : n.natAbs.Coprime d) → C { num := n, den := d, den_nz := nz, reduced := red }) : C a

Define a (dependent) function or prove ∀ r : Rat, p r by dealing with rational numbers of the form mk' n d with d ≠ 0.

@[simp]

theorem Rat.ofInt_ofNat {n : Nat} : ofInt (OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem Rat.ofInt_num {n : Int} : (ofInt n).num = n

@[simp]

theorem Rat.ofInt_den {n : Int} : (ofInt n).den = 1

@[simp]

theorem Rat.num_ofNat {n : Nat} : (OfNat.ofNat n).num = OfNat.ofNat n

@[simp]

theorem Rat.den_ofNat {n : Nat} : (OfNat.ofNat n).den = 1

@[simp]

theorem Rat.num_natCast (n : Nat) : (↑n).num = ↑n

@[simp]

theorem Rat.den_natCast (n : Nat) : (↑n).den = 1

@[reducible, inline, deprecated Rat.num_ofNat (since := "2025-08-22")]

abbrev Rat.ofNat_num {n : Nat} : (OfNat.ofNat n).num = OfNat.ofNat n

@[reducible, inline, deprecated Rat.den_ofNat (since := "2025-08-22")]

abbrev Rat.ofNat_den {n : Nat} : (OfNat.ofNat n).den = 1

theorem Rat.add_def (a b : Rat) : a + b = normalize (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den) ⋯

theorem Rat.add_def' (a b : Rat) : a + b = mkRat (a.num * ↑b.den + b.num * ↑a.den) (a.den * b.den)

theorem Rat.num_add (a b : Rat) : (a + b).num = (a.num * ↑b.den + b.num * ↑a.den) / ↑((a.num * ↑b.den + b.num * ↑a.den).natAbs.gcd (a.den * b.den))

theorem Rat.den_add (a b : Rat) : (a + b).den = a.den * b.den / (a.num * ↑b.den + b.num * ↑a.den).natAbs.gcd (a.den * b.den)

theorem Rat.add_zero (a : Rat) : a + 0 = a

theorem Rat.zero_add (a : Rat) : 0 + a = a

theorem Rat.normalize_add_normalize (n₁ n₂ : Int) {d₁ d₂ : Nat} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : normalize n₁ d₁ z₁ + normalize n₂ d₂ z₂ = normalize (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂) ⋯

theorem Rat.mkRat_add_mkRat (n₁ n₂ : Int) {d₁ d₂ : Nat} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : mkRat n₁ d₁ + mkRat n₂ d₂ = mkRat (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂)

@[simp]

theorem Rat.divInt_add_divInt (n₁ n₂ : Int) {d₁ d₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : divInt n₁ d₁ + divInt n₂ d₂ = divInt (n₁ * d₂ + n₂ * d₁) (d₁ * d₂)

theorem Rat.add_comm (a b : Rat) : a + b = b + a

theorem Rat.add_assoc (a b c : Rat) : a + b + c = a + (b + c)

theorem Rat.add_left_comm (a b c : Rat) : a + (b + c) = b + (a + c)

@[simp]

theorem Rat.neg_num (a : Rat) : (-a).num = -a.num

@[simp]

theorem Rat.neg_den (a : Rat) : (-a).den = a.den

theorem Rat.neg_normalize (n : Int) (d : Nat) (z : d ≠ 0) : -normalize n d z = normalize (-n) d z

theorem Rat.neg_mkRat (n : Int) (d : Nat) : -mkRat n d = mkRat (-n) d

@[simp]

theorem Rat.neg_divInt (n d : Int) : -divInt n d = divInt (-n) d

theorem Rat.neg_add_cancel (a : Rat) : -a + a = 0

theorem Rat.add_neg_cancel (a : Rat) : a + -a = 0

theorem Rat.add_right_cancel {a b : Rat} (c : Rat) (h : a + c = b + c) : a = b

theorem Rat.sub_def (a b : Rat) : a - b = normalize (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den) ⋯

theorem Rat.sub_def' (a b : Rat) : a - b = mkRat (a.num * ↑b.den - b.num * ↑a.den) (a.den * b.den)

theorem Rat.sub_eq_add_neg (a b : Rat) : a - b = a + -b

theorem Rat.neg_sub (a b : Rat) : -(a - b) = b - a

@[simp]

theorem Rat.divInt_sub_divInt (n₁ n₂ : Int) {d₁ d₂ : Int} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : divInt n₁ d₁ - divInt n₂ d₂ = divInt (n₁ * d₂ - n₂ * d₁) (d₁ * d₂)

theorem Rat.mul_def (a b : Rat) : a * b = normalize (a.num * b.num) (a.den * b.den) ⋯

theorem Rat.mul_def' (a b : Rat) : a * b = mkRat (a.num * b.num) (a.den * b.den)

theorem Rat.num_mul (a b : Rat) : (a * b).num = a.num * b.num / ↑((a.num * b.num).natAbs.gcd (a.den * b.den))

theorem Rat.den_mul (a b : Rat) : (a * b).den = a.den * b.den / (a.num * b.num).natAbs.gcd (a.den * b.den)

theorem Rat.mul_comm (a b : Rat) : a * b = b * a

@[simp]

theorem Rat.zero_mul (a : Rat) : 0 * a = 0

@[simp]

theorem Rat.mul_zero (a : Rat) : a * 0 = 0

@[simp]

theorem Rat.one_mul (a : Rat) : 1 * a = a

@[simp]

theorem Rat.mul_one (a : Rat) : a * 1 = a

theorem Rat.normalize_mul_normalize (n₁ n₂ : Int) {d₁ d₂ : Nat} (z₁ : d₁ ≠ 0) (z₂ : d₂ ≠ 0) : normalize n₁ d₁ z₁ * normalize n₂ d₂ z₂ = normalize (n₁ * n₂) (d₁ * d₂) ⋯

@[simp]

theorem Rat.mkRat_mul_mkRat (n₁ n₂ : Int) (d₁ d₂ : Nat) : mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)

theorem Rat.divInt_mul_divInt (n₁ n₂ : Int) {d₁ d₂ : Int} : divInt n₁ d₁ * divInt n₂ d₂ = divInt (n₁ * n₂) (d₁ * d₂)

theorem Rat.mul_assoc (a b c : Rat) : a * b * c = a * (b * c)

theorem Rat.add_mul (a b c : Rat) : (a + b) * c = a * c + b * c

theorem Rat.mul_add (a b c : Rat) : a * (b + c) = a * b + a * c

theorem Rat.neg_mul (a b : Rat) : -a * b = -(a * b)

theorem Rat.mul_neg (a b : Rat) : a * -b = -(a * b)

theorem Rat.inv_def (a : Rat) : a⁻¹ = divInt (↑a.den) a.num

@[simp]

theorem Rat.num_inv (a : Rat) : a⁻¹.num = a.num.sign * ↑a.den

@[simp]

theorem Rat.den_inv (a : Rat) : a⁻¹.den = if a.num = 0 then 1 else a.num.natAbs

@[simp]

theorem Rat.inv_zero : 0⁻¹ = 0

@[simp]

theorem Rat.inv_divInt (n d : Int) : (divInt n d)⁻¹ = divInt d n

theorem Rat.mul_inv_cancel (a : Rat) : a ≠ 0 → a * a⁻¹ = 1

theorem Rat.inv_mul_cancel (a : Rat) (h : a ≠ 0) : a⁻¹ * a = 1

theorem Rat.inv_eq_of_mul_eq_one {a b : Rat} (h : a * b = 1) : a⁻¹ = b

theorem Rat.inv_inv (a : Rat) : a⁻¹⁻¹ = a

theorem Rat.inv_mul_rev (a b : Rat) : (a * b)⁻¹ = b⁻¹ * a⁻¹

theorem Rat.mul_eq_zero {a b : Rat} : a * b = 0 ↔ a = 0 ∨ b = 0

theorem Rat.div_def (a b : Rat) : a / b = a * b⁻¹

theorem Rat.divInt_eq_div (a b : Int) : divInt a b = ↑a / ↑b

theorem Rat.mkRat_eq_div (a : Int) (b : Nat) : mkRat a b = ↑a / ↑b

theorem Rat.div_mul_cancel {a b : Rat} (hb : b ≠ 0) : a / b * b = a

theorem Rat.mul_div_cancel {a b : Rat} (hb : b ≠ 0) : a * b / b = a

theorem Rat.pow_def (q : Rat) (n : Nat) : q ^ n = { num := q.num ^ n, den := q.den ^ n, den_nz := ⋯, reduced := ⋯ }

@[simp]

theorem Rat.num_pow (q : Rat) (n : Nat) : (q ^ n).num = q.num ^ n

@[simp]

theorem Rat.den_pow (q : Rat) (n : Nat) : (q ^ n).den = q.den ^ n

@[simp]

theorem Rat.pow_zero (q : Rat) : q ^ 0 = 1

theorem Rat.pow_succ (q : Rat) (n : Nat) : q ^ (n + 1) = q ^ n * q

@[simp]

theorem Rat.pow_one (q : Rat) : q ^ 1 = q

@[simp]

theorem Rat.zpow_zero (q : Rat) : q ^ 0 = 1

@[simp]

theorem Rat.zpow_one (q : Rat) : q ^ 1 = q

theorem Rat.zpow_natCast (q : Rat) (n : Nat) : q ^ ↑n = q ^ n

theorem Rat.zpow_neg (q : Rat) (n : Int) : q ^ (-n) = (q ^ n)⁻¹

theorem Rat.zpow_add_one {q : Rat} (hq : q ≠ 0) (m : Int) : q ^ (m + 1) = q ^ m * q

theorem Rat.zpow_sub_one {q : Rat} (hq : q ≠ 0) (m : Int) : q ^ (m - 1) = q ^ m * q⁻¹

theorem Rat.zpow_add {q : Rat} (hq : q ≠ 0) (m n : Int) : q ^ (m + n) = q ^ m * q ^ n

ofScientific

theorem Rat.ofScientific_true_def {m e : Nat} : Rat.ofScientific m true e = mkRat (↑m) (10 ^ e)

theorem Rat.ofScientific_false_def {m e : Nat} : Rat.ofScientific m false e = ↑(m * 10 ^ e)

theorem Rat.ofScientific_def {m : Nat} {s : Bool} {e : Nat} : Rat.ofScientific m s e = if s = true then mkRat (↑m) (10 ^ e) else ↑(m * 10 ^ e)

@[simp]

theorem Rat.ofScientific_ofNat_ofNat {m : Nat} {s : Bool} {e : Nat} : Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) = OfScientific.ofScientific m s e

Rat.ofScientific applied to numeric literals is the same as a scientific literal.

≤ and <

@[simp]

theorem Rat.num_nonneg {q : Rat} : 0 ≤ q.num ↔ 0 ≤ q

@[simp]

theorem Rat.num_eq_zero {q : Rat} : q.num = 0 ↔ q = 0

theorem Rat.nonneg_antisymm {q : Rat} : 0 ≤ q → 0 ≤ -q → q = 0

theorem Rat.nonneg_total (a : Rat) : 0 ≤ a ∨ 0 ≤ -a

@[simp]

theorem Rat.divInt_nonneg_iff_of_pos_right {a b : Int} (hb : 0 < b) : 0 ≤ divInt a b ↔ 0 ≤ a

@[simp]

theorem Rat.divInt_nonneg {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ divInt a b

theorem Rat.add_nonneg {a b : Rat} : 0 ≤ a → 0 ≤ b → 0 ≤ a + b

theorem Rat.mul_nonneg {a b : Rat} : 0 ≤ a → 0 ≤ b → 0 ≤ a * b

theorem Rat.not_le {a b : Rat} : ¬a ≤ b ↔ b < a

theorem Rat.not_lt {a b : Rat} : ¬a < b ↔ b ≤ a

theorem Rat.lt_iff (a b : Rat) : a < b ↔ a.num * ↑b.den < b.num * ↑a.den

theorem Rat.le_iff (a b : Rat) : a ≤ b ↔ a.num * ↑b.den ≤ b.num * ↑a.den

theorem Rat.le_iff_sub_nonneg (a b : Rat) : a ≤ b ↔ 0 ≤ b - a

theorem Rat.le_total {a b : Rat} : a ≤ b ∨ b ≤ a

theorem Rat.le_refl {a : Rat} : a ≤ a

theorem Rat.le_trans {a b c : Rat} (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c

theorem Rat.le_antisymm {a b : Rat} (hab : a ≤ b) (hba : b ≤ a) : a = b

theorem Rat.le_of_lt {a b : Rat} (ha : a < b) : a ≤ b

@[simp]

theorem Rat.lt_irrefl {a : Rat} : ¬a < a

theorem Rat.ne_of_lt {a b : Rat} (ha : a < b) : a ≠ b

theorem Rat.ne_of_gt {a b : Rat} (ha : a < b) : b ≠ a

theorem Rat.lt_of_le_of_ne {a b : Rat} (ha : a ≤ b) (hb : a ≠ b) : a < b

theorem Rat.add_le_add_left {a b c : Rat} : c + a ≤ c + b ↔ a ≤ b

theorem Rat.add_le_add_right {a b c : Rat} : a + c ≤ b + c ↔ a ≤ b

theorem Rat.lt_iff_sub_pos (a b : Rat) : a < b ↔ 0 < b - a

theorem Rat.mul_pos {a b : Rat} (ha : 0 < a) (hb : 0 < b) : 0 < a * b

theorem Rat.mul_le_mul_of_nonneg_left {a b c : Rat} (ha : a ≤ b) (hc : 0 ≤ c) : c * a ≤ c * b

theorem Rat.mul_le_mul_of_nonneg_right {a b c : Rat} (ha : a ≤ b) (hc : 0 ≤ c) : a * c ≤ b * c

theorem Rat.mul_lt_mul_of_pos_left {a b c : Rat} (ha : a < b) (hc : 0 < c) : c * a < c * b

theorem Rat.mul_lt_mul_of_pos_right {a b c : Rat} (ha : a < b) (hc : 0 < c) : a * c < b * c

theorem Rat.le_of_mul_le_mul_left {a b c : Rat} (ha : c * a ≤ c * b) (hc : 0 < c) : a ≤ b

theorem Rat.le_of_mul_le_mul_right {a b c : Rat} (ha : a * c ≤ b * c) (hc : 0 < c) : a ≤ b

theorem Rat.lt_of_mul_lt_mul_left {a b c : Rat} (h : c * a < c * b) (hc : 0 ≤ c) : a < b

theorem Rat.lt_of_mul_lt_mul_right {a b c : Rat} (h : a * c < b * c) (hc : 0 ≤ c) : a < b

theorem Rat.mul_lt_mul_left {a b c : Rat} (hc : 0 < c) : c * a < c * b ↔ a < b

theorem Rat.mul_lt_mul_right {a b c : Rat} (hc : 0 < c) : a * c < b * c ↔ a < b

theorem Rat.mul_pos_iff_of_pos_left {a b : Rat} (ha : 0 < a) : 0 < a * b ↔ 0 < b

theorem Rat.mul_pos_iff_of_pos_right {a b : Rat} (hb : 0 < b) : 0 < a * b ↔ 0 < a

theorem Rat.mul_neg_iff_of_pos_left {a b : Rat} (ha : 0 < a) : a * b < 0 ↔ b < 0

theorem Rat.mul_neg_iff_of_pos_right {a b : Rat} (hb : 0 < b) : a * b < 0 ↔ a < 0

theorem Rat.inv_pos {a : Rat} : 0 < a⁻¹ ↔ 0 < a

theorem Rat.pow_pos {a : Rat} {n : Nat} (h : 0 < a) : 0 < a ^ n

theorem Rat.pow_nonneg {a : Rat} {n : Nat} (h : 0 ≤ a) : 0 ≤ a ^ n

theorem Rat.zpow_pos {a : Rat} {n : Int} (h : 0 < a) : 0 < a ^ n

theorem Rat.zpow_nonneg {a : Rat} {n : Int} (h : 0 ≤ a) : 0 ≤ a ^ n

theorem Rat.div_lt_iff {a b c : Rat} (hb : 0 < b) : a / b < c ↔ a < c * b

theorem Rat.div_lt_iff' {a b c : Rat} (hb : 0 < b) : a / b < c ↔ a < b * c

theorem Rat.lt_div_iff {a b c : Rat} (hc : 0 < c) : a < b / c ↔ a * c < b

theorem Rat.lt_div_iff' {a b c : Rat} (hc : 0 < c) : a < b / c ↔ c * a < b

intCast

@[simp]

theorem Rat.den_intCast (a : Int) : (↑a).den = 1

@[simp]

theorem Rat.num_intCast (a : Int) : (↑a).num = a

@[reducible, inline, deprecated Rat.den_intCast (since := "2025-08-22")]

abbrev Rat.intCast_den (a : Int) : (↑a).den = 1

@[reducible, inline, deprecated Rat.num_intCast (since := "2025-08-22")]

abbrev Rat.intCast_num (a : Int) : (↑a).num = a

The following lemmas are later subsumed by e.g. Int.cast_add and Int.cast_mul in Mathlib but it is convenient to have these earlier, for users who only need Int and Rat.

theorem Rat.intCast_natCast (n : Nat) : ↑↑n = ↑n

@[simp]

theorem Rat.intCast_inj {a b : Int} : ↑a = ↑b ↔ a = b

@[simp]

theorem Rat.natCast_inj {a b : Nat} : ↑a = ↑b ↔ a = b

@[simp]

theorem Rat.intCast_eq_zero_iff {a : Int} : ↑a = 0 ↔ a = 0

@[simp]

theorem Rat.natCast_eq_zero_iff {a : Nat} : ↑a = 0 ↔ a = 0

@[simp]

theorem Rat.ofNat_eq_ofNat {a b : Nat} : OfNat.ofNat a = OfNat.ofNat b ↔ a = b

@[simp]

theorem Rat.intCast_ofNat {a : Nat} : ↑(OfNat.ofNat a) = OfNat.ofNat a

@[simp]

theorem Rat.natCast_ofNat {a : Nat} : ↑(OfNat.ofNat a) = OfNat.ofNat a

theorem Rat.intCast_zero : ↑0 = 0

theorem Rat.intCast_one : ↑1 = 1

@[simp]

theorem Rat.intCast_add (a b : Int) : ↑(a + b) = ↑a + ↑b

@[simp]

theorem Rat.natCast_add (a b : Nat) : ↑(a + b) = ↑a + ↑b

@[simp]

theorem Rat.intCast_neg (a : Int) : ↑(-a) = -↑a

@[simp]

theorem Rat.intCast_sub (a b : Int) : ↑(a - b) = ↑a - ↑b

@[simp]

theorem Rat.intCast_mul (a b : Int) : ↑(a * b) = ↑a * ↑b

@[simp]

theorem Rat.natCast_mul (a b : Nat) : ↑(a * b) = ↑a * ↑b

@[simp]

theorem Rat.intCast_pow (a : Int) (n : Nat) : ↑(a ^ n) = ↑a ^ n

@[simp]

theorem Rat.natCast_pow (a b : Nat) : ↑(a ^ b) = ↑a ^ b

theorem Rat.intCast_le_intCast {a b : Int} : ↑a ≤ ↑b ↔ a ≤ b

theorem Rat.intCast_lt_intCast {a b : Int} : ↑a < ↑b ↔ a < b

theorem Rat.natCast_le_natCast {a b : Nat} : ↑a ≤ ↑b ↔ a ≤ b

theorem Rat.natCast_lt_natCast {a b : Nat} : ↑a < ↑b ↔ a < b

theorem Rat.intCast_nonneg {a : Int} : 0 ≤ ↑a ↔ 0 ≤ a

theorem Rat.natCast_nonneg {a : Nat} : 0 ≤ ↑a

theorem Rat.intCast_pos {a : Int} : 0 < ↑a ↔ 0 < a

theorem Rat.natCast_pos {a : Nat} : 0 < ↑a ↔ 0 < a

theorem Rat.intCast_nonpos {a : Int} : ↑a ≤ 0 ↔ a ≤ 0

theorem Rat.intCast_neg_iff {a : Int} : ↑a < 0 ↔ a < 0

theorem Rat.ofScientific_def' {m : Nat} {s : Bool} {e : Nat} : OfScientific.ofScientific m s e = ↑m * 10 ^ if s = true then -↑e else ↑e

Alternative statement of ofScientific_def.

theorem Rat.ofScientific_def_eq_if {m : Nat} {s : Bool} {e : Nat} : OfScientific.ofScientific m s e = if s = true then ↑m / 10 ^ e else ↑m * 10 ^ e

min and max

theorem Rat.max_def {n m : Rat} : max n m = if n ≤ m then m else n

theorem Rat.min_def {n m : Rat} : min n m = if n ≤ m then n else m

floor

theorem Rat.floor_def (a : Rat) : a.floor = a.num / ↑a.den

@[simp]

theorem Rat.floor_intCast (a : Int) : (↑a).floor = a

theorem Rat.floor_monotone {a b : Rat} (h : a ≤ b) : a.floor ≤ b.floor

theorem Rat.floor_le (a : Rat) : ↑a.floor ≤ a

theorem Rat.lt_floor_add_one (a : Rat) : a < ↑(a.floor + 1)

theorem Rat.le_floor_iff {x : Int} {a : Rat} : x ≤ a.floor ↔ ↑x ≤ a

theorem Rat.floor_lt_iff {a : Rat} {x : Int} : a.floor < x ↔ a < ↑x

theorem Rat.ceil_eq_neg_floor_neg (a : Rat) : a.ceil = -(-a).floor

@[simp]

theorem Rat.ceil_intCast (a : Int) : (↑a).ceil = a