mathlib documentation

data.rat.order

Order for Rational Numbers #

Summary #

We define the order on ℚ, prove that ℚ is a discrete, linearly ordered field, and define functions such as abs and sqrt that depend on this order.

Notations #

Tags #

rat, rationals, field, ℚ, numerator, denominator, num, denom, order, ordering, sqrt, abs

source
@[protected]
def rat.nonneg (r : ℚ) :
Prop

A rational number is called nonnegative if its numerator is nonnegative.

Equations
source
@[simp]
theorem rat.mk_nonneg (a : ℤ) {b : ℤ} (h : 0 < b) :
(a /. b).nonneg ↔ 0 ≤ a
source
@[protected]
theorem rat.nonneg_add {a b : ℚ} :
a.nonneg → b.nonneg → (a + b).nonneg
source
@[protected]
theorem rat.nonneg_mul {a b : ℚ} :
a.nonneg → b.nonneg → (a * b).nonneg
source
@[protected]
theorem rat.nonneg_antisymm {a : ℚ} :
a.nonneg → (-a).nonneg → a = 0
source
@[protected]
theorem rat.nonneg_total (a : ℚ) :
a.nonneg ∨ (-a).nonneg
source
@[protected, instance]
def rat.decidable_nonneg (a : ℚ) :
decidable a.nonneg
Equations
source
@[protected]
def rat.le (a b : ℚ) :
Prop

Relation a ≤ b on ℚ defined as a ≤ b ↔ rat.nonneg (b - a). Use a ≤ b instead of rat.le a b.

Equations
source
@[protected, instance]
def rat.has_le  :
has_le ℚ
Equations
source
@[protected, instance]
def rat.decidable_le  :
decidable_rel has_le.le
Equations
source
@[protected]
theorem rat.le_def {a b c d : ℤ} (b0 : 0 < b) (d0 : 0 < d) :
a /. b ≤ c /. d ↔ a * d ≤ c * b
source
@[protected]
theorem rat.le_refl (a : ℚ) :
a ≤ a
source
@[protected]
theorem rat.le_total (a b : ℚ) :
a ≤ b ∨ b ≤ a
source
@[protected]
theorem rat.le_antisymm {a b : ℚ} (hab : a ≤ b) (hba : b ≤ a) :
a = b
source
@[protected]
theorem rat.le_trans {a b c : ℚ} (hab : a ≤ b) (hbc : b ≤ c) :
a ≤ c
source
@[protected, instance]
def rat.linear_order  :
linear_order ℚ
Equations
source
@[protected, instance]
def rat.has_lt  :
has_lt ℚ
Equations
source
@[protected, instance]
def rat.distrib_lattice  :
distrib_lattice ℚ
Equations
source
@[protected, instance]
def rat.lattice  :
lattice ℚ
Equations
source
@[protected, instance]
def rat.semilattice_inf  :
semilattice_inf ℚ
Equations
source
@[protected, instance]
def rat.semilattice_sup  :
semilattice_sup ℚ
Equations
source
@[protected, instance]
def rat.has_inf  :
has_inf ℚ
Equations
source
@[protected, instance]
def rat.has_sup  :
has_sup ℚ
Equations
source
@[protected, instance]
def rat.partial_order  :
partial_order ℚ
Equations
source
@[protected, instance]
def rat.preorder  :
preorder ℚ
Equations
source
@[protected]
theorem rat.le_def' {p q : ℚ} :
p ≤ q ↔ (p.num) * ↑(q.denom) ≤ (q.num) * ↑(p.denom)
source
@[protected]
theorem rat.lt_def {p q : ℚ} :
p < q ↔ (p.num) * ↑(q.denom) < (q.num) * ↑(p.denom)
source
theorem rat.nonneg_iff_zero_le {a : ℚ} :
a.nonneg ↔ 0 ≤ a
source
theorem rat.num_nonneg_iff_zero_le {a : ℚ} :
0 ≤ a.num ↔ 0 ≤ a
source
@[protected]
theorem rat.add_le_add_left {a b c : ℚ} :
c + a ≤ c + b ↔ a ≤ b
source
@[protected]
theorem rat.mul_nonneg {a b : ℚ} (ha : 0 ≤ a) (hb : 0 ≤ b) :
0 ≤ a * b
source
@[protected, instance]
def rat.linear_ordered_field  :
linear_ordered_field ℚ
Equations
source
@[protected, instance]
def rat.linear_ordered_comm_ring  :
linear_ordered_comm_ring ℚ
Equations
source
@[protected, instance]
def rat.linear_ordered_ring  :
linear_ordered_ring ℚ
Equations
source
@[protected, instance]
def rat.ordered_ring  :
ordered_ring ℚ
Equations
source
@[protected, instance]
def rat.linear_ordered_semiring  :
linear_ordered_semiring ℚ
Equations
source
@[protected, instance]
def rat.ordered_semiring  :
ordered_semiring ℚ
Equations
source
@[protected, instance]
def rat.linear_ordered_add_comm_group  :
linear_ordered_add_comm_group ℚ
Equations
source
@[protected, instance]
def rat.ordered_add_comm_group  :
ordered_add_comm_group ℚ
Equations
source
@[protected, instance]
def rat.ordered_cancel_add_comm_monoid  :
ordered_cancel_add_comm_monoid ℚ
Equations
source
@[protected, instance]
def rat.ordered_add_comm_monoid  :
ordered_add_comm_monoid ℚ
Equations
source
theorem rat.num_pos_iff_pos {a : ℚ} :
0 < a.num ↔ 0 < a
source
theorem rat.div_lt_div_iff_mul_lt_mul {a b c d : ℤ} (b_pos : 0 < b) (d_pos : 0 < d) :
↑a / ↑b < ↑c / ↑d ↔ a * d < c * b
source
theorem rat.lt_one_iff_num_lt_denom {q : ℚ} :
q < 1 ↔ q.num < ↑(q.denom)
source
theorem rat.abs_def (q : ℚ) :
|q| = ↑(q.num.nat_abs) /. ↑(q.denom)