Documentation

Init.Grind.Ordered.Int

← Copula mathematical handbook

grind instances for Int as an ordered module. #

source
instance Lean.Grind.instIsLinearOrderInt :
Std.IsLinearOrder Int
source
instance Lean.Grind.instLawfulOrderLTInt :
Std.LawfulOrderLT Int
source
instance Lean.Grind.instOrderedAddInt :
OrderedAdd Int
source
instance Lean.Grind.instOrderedRingInt :
OrderedRing Int