Basics for the Rational Numbers #
We define the integral domain structure on
ℚ and prove basic lemmas about it.
The definition of the field structure on
ℚ will be done in
Mathlib.Data.Rat.Basic once the
Field class has been defined.
Main Definitions #
Rat.divInt n dconstructs a rational number
q = n / dfrom
n d : ℤ.
/.is infix notation for
At this point in the import hierarchy we have not defined the
Instead we'll instantiate
CommGroupWithZero at this point.
Rat.field instance and any field-specific lemmas can be found in