We define the canonical injection from ℚ into an arbitrary division ring and prove various casting lemmas showing the well-behavedness of this injection.
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 p, we define 1 / p = 1 / 0 = 0 for consistency with our division by zero convention.