Casts for Rational Numbers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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
ℚ as an order embedding.
g agree on the integers then they are equal
Positive integer values of a morphism
φ and its value on
-1 completely determine
Any two ring homomorphisms from
ℚ to a semiring are equal. If the codomain is a division ring,
then this lemma follows from