← Mathematical handbook

grind instances for Rat as an ordered module.

instance Lean.Grind.instIsLinearOrderRat : Std.IsLinearOrder Rat

instance Lean.Grind.instLawfulOrderLTRat : Std.LawfulOrderLT Rat

instance Lean.Grind.instOrderedAddRat : OrderedAdd Rat

instance Lean.Grind.instOrderedRingRat : OrderedRing Rat