TorchLean API
Docs Home
Guide
Examples
Graphs
Init
.
GrindInstances
.
Ring
.
Rat
Search
Declaration colors
def
theorem
structure
axiom
return to top
source
Imports
Init.Data.Int.Lemmas
Init.Data.Rat.Lemmas
Init.Grind.Ring.OfScientific
Init.Data.Int.DivMod.Lemmas
Imported by
Lean
.
Grind
.
instFieldRat
Lean
.
Grind
.
instIsCharPRatOfNatNat
Lean
.
Grind
.
instNoNatZeroDivisorsRat
Lean
.
Grind
.
instLawfulOfScientificRat
source
@[implicit_reducible]
instance
Lean
.
Grind
.
instFieldRat
:
Field
Rat
source
instance
Lean
.
Grind
.
instIsCharPRatOfNatNat
:
IsCharP
Rat
0
source
instance
Lean
.
Grind
.
instNoNatZeroDivisorsRat
:
NoNatZeroDivisors
Rat
source
instance
Lean
.
Grind
.
instLawfulOfScientificRat
:
LawfulOfScientific
Rat