Documentation
Init
.
Grind
.
Ordered
.
Rat
Search
return to top
source
Imports
Init.Data.Rat.Lemmas
Init.Grind.Ordered.Ring
Init.GrindInstances.Ring.Rat
Imported by
Lean
.
Grind
.
instIsLinearOrderRat
Lean
.
Grind
.
instLawfulOrderLTRat
Lean
.
Grind
.
instOrderedAddRat
Lean
.
Grind
.
instOrderedRingRat
grind
instances for
Rat
as an ordered module.
#
source
instance
Lean
.
Grind
.
instIsLinearOrderRat
:
Std.IsLinearOrder
Rat
source
instance
Lean
.
Grind
.
instLawfulOrderLTRat
:
Std.LawfulOrderLT
Rat
source
instance
Lean
.
Grind
.
instOrderedAddRat
:
OrderedAdd
Rat
source
instance
Lean
.
Grind
.
instOrderedRingRat
:
OrderedRing
Rat