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
@[simp]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp]
@[simp, norm_cast]
@[simp, norm_cast]
Coercion from ℚ
as an order embedding.
@[simp]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp, norm_cast]
theorem
rat.cast_min
{K : Type u_5}
[linear_ordered_field K]
{a b : ℚ} :
↑(linear_order.min a b) = linear_order.min ↑a ↑b
@[simp, norm_cast]
theorem
rat.cast_max
{K : Type u_5}
[linear_ordered_field K]
{a b : ℚ} :
↑(linear_order.max a b) = linear_order.max ↑a ↑b
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
map_rat_cast
{F : Type u_1}
{α : Type u_3}
{β : Type u_4}
[division_ring α]
[division_ring β]
[ring_hom_class F α β]
(f : F)
(q : ℚ) :
@[simp]
theorem
eq_rat_cast
{F : Type u_1}
{k : Type u_2}
[division_ring k]
[ring_hom_class F ℚ k]
(f : F)
(r : ℚ) :
theorem
monoid_with_zero_hom.ext_rat'
{F : Type u_1}
{M₀ : Type u_5}
[monoid_with_zero M₀]
[monoid_with_zero_hom_class F ℚ M₀]
{f g : F}
(h : ∀ (m : ℤ), ⇑f ↑m = ⇑g ↑m) :
f = g
If f
and g
agree on the integers then they are equal φ
.
@[ext]
theorem
monoid_with_zero_hom.ext_rat
{M₀ : Type u_5}
[monoid_with_zero M₀]
{f g : ℚ →*₀ M₀}
(h : f.comp ↑(int.cast_ring_hom ℚ) = g.comp ↑(int.cast_ring_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.
theorem
monoid_with_zero_hom.ext_rat_on_pnat
{F : Type u_1}
{M₀ : Type u_5}
[monoid_with_zero M₀]
[monoid_with_zero_hom_class F ℚ M₀]
{f g : F}
(same_on_neg_one : ⇑f (-1) = ⇑g (-1))
(same_on_pnat : ∀ (n : ℕ), 0 < n → ⇑f ↑n = ⇑g ↑n) :
f = g
Positive integer values of a morphism φ
and its value on -1
completely determine φ
.
theorem
ring_hom.ext_rat
{F : Type u_1}
{R : Type u_2}
[semiring R]
[ring_hom_class F ℚ R]
(f g : F) :
f = g
Any two ring homomorphisms from ℚ
to a semiring are equal. If the codomain is a division ring,
then this lemma follows from eq_rat_cast
.
@[protected, instance]
@[simp, norm_cast]
@[simp, norm_cast]
theorem
mul_opposite.unop_rat_cast
{α : Type u_3}
[division_ring α]
(r : ℚ) :
mul_opposite.unop ↑r = ↑r