Documentation

Init.GrindInstances.Ring.Nat

source
@[implicit_reducible]
instance Lean.Grind.instCommSemiringNat :
CommSemiring Nat
source
instance Lean.Grind.instIsPreorderNat :
Std.IsPreorder Nat
source
instance Lean.Grind.instLawfulOrderLTNat :
Std.LawfulOrderLT Nat
source
instance Lean.Grind.instOrderedRingNat :
OrderedRing Nat
source
instance Lean.Grind.instIsCharPNatOfNat :
IsCharP Nat 0
source
instance Lean.Grind.instNoNatZeroDivisorsNat :
NoNatZeroDivisors Nat