Casts for Rational Numbers #
We define the canonical injection from ℚ into an arbitrary division ring and prove various casting lemmas showing the well-behavedness of this injection.
/.is infix notation for
rat, rationals, field, ℚ, numerator, denominator, num, denom, cast, coercion, casting
Construct the canonical injection from
ℚ into an arbitrary
division ring. If the field has positive characteristic
1 / p = 1 / 0 = 0 for consistency with our
division by zero convention.
g agree on the integers then they are equal
See note [partially-applied ext lemmas] for why
comp is used here.