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
g agree on the integers then they are equal
See note [partially-applied ext lemmas] for why
comp is used here.
Positive integer values of a morphism
φ and its value on
-1 completely determine