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
@[protected, 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, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp]
@[simp]
@[simp]
@[simp, norm_cast]
theorem
rat.cast_min
{α : Type u_2}
[linear_ordered_field α]
{a b : ℚ} :
↑(linear_order.min a b) = linear_order.min ↑a ↑b
@[simp, norm_cast]
theorem
rat.cast_max
{α : Type u_2}
[linear_ordered_field α]
{a b : ℚ} :
↑(linear_order.max a b) = linear_order.max ↑a ↑b
@[simp]
theorem
map_rat_cast
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[division_ring α]
[division_ring β]
[char_zero α]
[ring_hom_class F α β]
(f : F)
(q : ℚ) :
@[protected, instance]
@[ext]
theorem
monoid_with_zero_hom.ext_rat
{M : Type u_4}
[group_with_zero M]
{f g : ℚ →*₀ M}
(same_on_int : f.comp (int.cast_ring_hom ℚ).to_monoid_with_zero_hom = g.comp (int.cast_ring_hom ℚ).to_monoid_with_zero_hom) :
f = g
If f
and g
agree on the integers then they are equal φ
.
See note [partially-applied ext lemmas] for why comp
is used here.
@[simp, norm_cast]
@[simp, norm_cast]
theorem
mul_opposite.unop_rat_cast
{α : Type u_2}
[division_ring α]
(r : ℚ) :
mul_opposite.unop ↑r = ↑r