The rational numbers form a linear ordered field

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

instance Rat.instLinearOrderedCommRing : LinearOrderedCommRing ℚ

Equations

• Rat.instLinearOrderedCommRing = let __spread.0 := Rat.linearOrder; let __spread.1 := Rat.commRing; LinearOrderedCommRing.mk ⋯

instance Rat.instLinearOrderedRing : LinearOrderedRing ℚ

Equations

• Rat.instLinearOrderedRing = inferInstance

instance Rat.instOrderedRing : OrderedRing ℚ

Equations

• Rat.instOrderedRing = inferInstance

instance Rat.instLinearOrderedSemiring : LinearOrderedSemiring ℚ

Equations

• Rat.instLinearOrderedSemiring = inferInstance

instance Rat.instOrderedSemiring : OrderedSemiring ℚ

Equations

• Rat.instOrderedSemiring = inferInstance

instance Rat.instLinearOrderedAddCommGroup : LinearOrderedAddCommGroup ℚ

Equations

• Rat.instLinearOrderedAddCommGroup = inferInstance

instance Rat.instOrderedAddCommGroup : OrderedAddCommGroup ℚ

Equations

• Rat.instOrderedAddCommGroup = inferInstance

instance Rat.instOrderedCancelAddCommMonoid : OrderedCancelAddCommMonoid ℚ

Equations

• Rat.instOrderedCancelAddCommMonoid = inferInstance

instance Rat.instOrderedAddCommMonoid : OrderedAddCommMonoid ℚ

Equations

• Rat.instOrderedAddCommMonoid = inferInstance