Documentation

Init.GrindInstances.Ring.Nat

source
instance Lean.Grind.instCommSemiringNat :
CommSemiring Nat
Equations
    source
    instance Lean.Grind.instPreorderNat :
    Preorder Nat
    Equations
      source
      instance Lean.Grind.instOrderedRingNat :
      OrderedRing Nat
      source
      instance Lean.Grind.instIsCharPNatOfNat :
      IsCharP Nat 0
      source
      instance Lean.Grind.instNoNatZeroDivisorsNat :
      NoNatZeroDivisors Nat