Casts for Rational Numbers
Summary
We define the canonical injection from ℚ into an arbitrary division ring and prove various casting lemmas showing the well-behavedness of this injection.
Notations
/.is infix notation forrat.mk.
Tags
rat, rationals, field, ℚ, numerator, denominator, num, denom, cast, coercion, casting
@[instance]
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.
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
ring_hom.map_rat_cast
{k : Type u_1}
{k' : Type u_2}
[division_ring k]
[char_zero k]
[division_ring k']
(f : k →+* k')
(r : ℚ) :
@[instance]