Order for Rational Numbers #
This file constructs the order on ℚ
and proves that ℚ
is a discrete, linearly ordered
commutative ring.
ℚ
is in fact a linearly ordered field, but this fact is located in Data.Rat.Field
instead of
here because we need the order on ℚ
to define ℚ≥0
, which we itself need to define Field
.
Tags #
rat, rationals, field, ℚ, numerator, denominator, num, denom, order, ordering
@[simp]
@[simp]
theorem
Rat.divInt_le_divInt
{a : ℤ}
{b : ℤ}
{c : ℤ}
{d : ℤ}
(b0 : 0 < b)
(d0 : 0 < d)
:
Rat.divInt a b ≤ Rat.divInt c d ↔ a * d ≤ c * b
Equations
- One or more equations did not get rendered due to their size.
Equations
- Rat.instDistribLatticeRat = inferInstance
Equations
- Rat.instSemilatticeInfRat = inferInstance
Equations
- Rat.instSemilatticeSupRat = inferInstance
Equations
- Rat.instPartialOrderRat = inferInstance
Equations
- Rat.instLinearOrderedCommRing = let __spread.0 := Rat.linearOrder; let __spread.1 := Rat.commRing; LinearOrderedCommRing.mk ⋯
Equations
- Rat.instLinearOrderedRingRat = inferInstance
Equations
- Rat.instLinearOrderedSemiringRat = inferInstance
Equations
- Rat.instOrderedSemiringRat = inferInstance
Equations
- Rat.instLinearOrderedAddCommGroupRat = inferInstance
Equations
- Rat.instOrderedAddCommGroupRat = inferInstance
Equations
- Rat.instOrderedCancelAddCommMonoidRat = inferInstance
Equations
- Rat.instOrderedAddCommMonoidRat = inferInstance
@[deprecated Rat.num_nonneg]
Alias of Rat.num_nonneg
.
@[deprecated Rat.num_pos]
Alias of Rat.num_pos
.