source
instance Lean.Grind.instCommSemiringNat :
CommSemiring Nat
Equations

- One or more equations did not get rendered due to their size.

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