Documentation
Init
.
GrindInstances
.
Ring
.
Int
Search
return to top
source
Imports
Init.Meta
Init.Data.Int.Lemmas
Init.Data.Int.Pow
Init.Grind.Ring.Basic
Init.Data.Int.DivMod.Lemmas
Imported by
Lean
.
Grind
.
instCommRingInt
Lean
.
Grind
.
instIsCharPIntOfNatNat
Lean
.
Grind
.
instNoNatZeroDivisorsInt
source
@[implicit_reducible]
instance
Lean
.
Grind
.
instCommRingInt
:
CommRing
Int
source
instance
Lean
.
Grind
.
instIsCharPIntOfNatNat
:
IsCharP
Int
0
source
instance
Lean
.
Grind
.
instNoNatZeroDivisorsInt
:
NoNatZeroDivisors
Int