Bundled ordered algebra structures on ℚ≥0

instance instNNRatOrderedCommSemiring : OrderedCommSemiring ℚ≥0

Equations

• instNNRatOrderedCommSemiring = Nonneg.orderedCommSemiring

instance instNNRatLinearOrderedAddCommMonoid : LinearOrderedAddCommMonoid ℚ≥0

Equations

• instNNRatLinearOrderedAddCommMonoid = Nonneg.linearOrderedAddCommMonoid

instance NNRat.instOrderedSub : OrderedSub ℚ≥0

instance NNRat.instCanonicallyOrderedAdd : CanonicallyOrderedAdd ℚ≥0