Documentation
Mathlib
.
Data
.
NNRat
.
Order
Search
Google site search
return to top
source
Imports
Init
Mathlib.Data.NNRat.Defs
Mathlib.Algebra.Order.Nonneg.Ring
Mathlib.Algebra.Order.Ring.Rat
Imported by
NNRat
.
instOrderedSub
Bundled ordered algebra structures on
ℚ≥0
#
source
instance
NNRat
.
instOrderedSub
:
OrderedSub
ℚ≥0
Equations
NNRat.instOrderedSub
=
⋯