Documentation
Init
.
GrindInstances
.
Ring
.
Rat
Search
return to top
source
Imports
Init.Data.Rat.Lemmas
Init.Grind.Ring.Field
Imported by
Lean
.
Grind
.
instFieldRat
Lean
.
Grind
.
instIsCharPRatOfNatNat
Lean
.
Grind
.
instNoNatZeroDivisorsRat
source
instance
Lean
.
Grind
.
instFieldRat
:
Field
Rat
Equations
One or more equations did not get rendered due to their size.
source
instance
Lean
.
Grind
.
instIsCharPRatOfNatNat
:
IsCharP
Rat
0
source
instance
Lean
.
Grind
.
instNoNatZeroDivisorsRat
:
NoNatZeroDivisors
Rat