Bundled ordered algebra structures on ℚ≥0

instance instNNRatCanonicallyOrderedCommSemiring : CanonicallyOrderedCommSemiring ℚ≥0

Equations

• instNNRatCanonicallyOrderedCommSemiring = Nonneg.canonicallyOrderedCommSemiring

instance instNNRatCanonicallyLinearOrderedAddCommMonoid : CanonicallyLinearOrderedAddCommMonoid ℚ≥0

Equations

• instNNRatCanonicallyLinearOrderedAddCommMonoid = Nonneg.canonicallyLinearOrderedAddCommMonoid

instance NNRat.instOrderedSub : OrderedSub ℚ≥0

Equations

• NNRat.instOrderedSub = ⋯