data.rat.cast

# 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 for rat.mk.

## Tags #

rat, rationals, field, ℚ, numerator, denominator, num, denom, cast, coercion, casting

@[simp]
theorem rat.cast_of_int {α : Type u_3} (n : ) :
@[simp, norm_cast]
theorem rat.cast_coe_int {α : Type u_3} (n : ) :
@[simp, norm_cast]
theorem rat.cast_coe_nat {α : Type u_3} (n : ) :
@[simp, norm_cast]
theorem rat.cast_zero {α : Type u_3}  :
0 = 0
@[simp, norm_cast]
theorem rat.cast_one {α : Type u_3}  :
1 = 1
theorem rat.cast_commute {α : Type u_3} (r : ) (a : α) :
a
theorem rat.cast_comm {α : Type u_3} (r : ) (a : α) :
r * a = a * r
theorem rat.commute_cast {α : Type u_3} (a : α) (r : ) :
r
@[norm_cast]
theorem rat.cast_mk_of_ne_zero {α : Type u_3} (a b : ) (b0 : b 0) :
(rat.mk a b) = a / b
@[norm_cast]
theorem rat.cast_add_of_ne_zero {α : Type u_3} {m n : } :
(m.denom) 0(n.denom) 0(m + n) = m + n
@[simp, norm_cast]
theorem rat.cast_neg {α : Type u_3} (n : ) :
@[norm_cast]
theorem rat.cast_sub_of_ne_zero {α : Type u_3} {m n : } (m0 : (m.denom) 0) (n0 : (n.denom) 0) :
(m - n) = m - n
@[norm_cast]
theorem rat.cast_mul_of_ne_zero {α : Type u_3} {m n : } :
(m.denom) 0(n.denom) 0(m * n) = m * n
@[simp]
theorem rat.cast_inv_nat {α : Type u_3} (n : ) :
@[simp]
theorem rat.cast_inv_int {α : Type u_3} (n : ) :
@[norm_cast]
theorem rat.cast_inv_of_ne_zero {α : Type u_3} {n : } :
(n.num) 0(n.denom) 0n⁻¹ = (n)⁻¹
@[norm_cast]
theorem rat.cast_div_of_ne_zero {α : Type u_3} {m n : } (md : (m.denom) 0) (nn : (n.num) 0) (nd : (n.denom) 0) :
(m / n) = m / n
@[simp, norm_cast]
theorem rat.cast_inj {α : Type u_3} [char_zero α] {m n : } :
m = n m = n
theorem rat.cast_injective {α : Type u_3} [char_zero α] :
@[simp]
theorem rat.cast_eq_zero {α : Type u_3} [char_zero α] {n : } :
n = 0 n = 0
theorem rat.cast_ne_zero {α : Type u_3} [char_zero α] {n : } :
n 0 n 0
@[simp, norm_cast]
theorem rat.cast_add {α : Type u_3} [char_zero α] (m n : ) :
(m + n) = m + n
@[simp, norm_cast]
theorem rat.cast_sub {α : Type u_3} [char_zero α] (m n : ) :
(m - n) = m - n
@[simp, norm_cast]
theorem rat.cast_mul {α : Type u_3} [char_zero α] (m n : ) :
(m * n) = m * n
@[simp, norm_cast]
theorem rat.cast_bit0 {α : Type u_3} [char_zero α] (n : ) :
(bit0 n) =
@[simp, norm_cast]
theorem rat.cast_bit1 {α : Type u_3} [char_zero α] (n : ) :
(bit1 n) =
def rat.cast_hom (α : Type u_3) [char_zero α] :

Coercion ℚ → α as a ring_hom.

Equations
@[simp]
theorem rat.coe_cast_hom {α : Type u_3} [char_zero α] :
@[simp, norm_cast]
theorem rat.cast_inv {α : Type u_3} [char_zero α] (n : ) :
@[simp, norm_cast]
theorem rat.cast_div {α : Type u_3} [char_zero α] (m n : ) :
(m / n) = m / n
@[norm_cast]
theorem rat.cast_mk {α : Type u_3} [char_zero α] (a b : ) :
(rat.mk a b) = a / b
@[simp, norm_cast]
theorem rat.cast_pow {α : Type u_3} [char_zero α] (q : ) (k : ) :
(q ^ k) = q ^ k
@[simp, norm_cast]
theorem rat.cast_list_sum {α : Type u_3} [char_zero α] (s : list ) :
(s.sum) = s).sum
@[simp, norm_cast]
theorem rat.cast_multiset_sum {α : Type u_3} [char_zero α] (s : multiset ) :
(s.sum) = s).sum
@[simp, norm_cast]
theorem rat.cast_sum {ι : Type u_2} {α : Type u_3} [char_zero α] (s : finset ι) (f : ι → ) :
(s.sum (λ (i : ι), f i)) = s.sum (λ (i : ι), (f i))
@[simp, norm_cast]
theorem rat.cast_list_prod {α : Type u_3} [char_zero α] (s : list ) :
(s.prod) = s).prod
@[simp, norm_cast]
theorem rat.cast_multiset_prod {α : Type u_3} [field α] [char_zero α] (s : multiset ) :
(s.prod) = s).prod
@[simp, norm_cast]
theorem rat.cast_prod {ι : Type u_2} {α : Type u_3} [field α] [char_zero α] (s : finset ι) (f : ι → ) :
(s.prod (λ (i : ι), f i)) = s.prod (λ (i : ι), (f i))
theorem rat.cast_pos_of_pos {K : Type u_5} {r : } (hr : 0 < r) :
0 < r
theorem rat.cast_strict_mono {K : Type u_5}  :
theorem rat.cast_mono {K : Type u_5}  :
def rat.cast_order_embedding {K : Type u_5}  :

Coercion from ℚ as an order embedding.

Equations
@[simp]
theorem rat.cast_order_embedding_apply {K : Type u_5} (ᾰ : ) :
@[simp, norm_cast]
theorem rat.cast_le {K : Type u_5} {m n : } :
m n m n
@[simp, norm_cast]
theorem rat.cast_lt {K : Type u_5} {m n : } :
m < n m < n
@[simp]
theorem rat.cast_nonneg {K : Type u_5} {n : } :
0 n 0 n
@[simp]
theorem rat.cast_nonpos {K : Type u_5} {n : } :
n 0 n 0
@[simp]
theorem rat.cast_pos {K : Type u_5} {n : } :
0 < n 0 < n
@[simp]
theorem rat.cast_lt_zero {K : Type u_5} {n : } :
n < 0 n < 0
@[simp, norm_cast]
theorem rat.cast_min {K : Type u_5} {a b : } :
b) =
@[simp, norm_cast]
theorem rat.cast_max {K : Type u_5} {a b : } :
b) =
@[simp, norm_cast]
theorem rat.cast_abs {K : Type u_5} {q : } :
@[simp]
theorem rat.preimage_cast_Icc {K : Type u_5} (a b : ) :
@[simp]
theorem rat.preimage_cast_Ico {K : Type u_5} (a b : ) :
@[simp]
theorem rat.preimage_cast_Ioc {K : Type u_5} (a b : ) :
@[simp]
theorem rat.preimage_cast_Ioo {K : Type u_5} (a b : ) :
@[simp]
theorem rat.preimage_cast_Ici {K : Type u_5} (a : ) :
=
@[simp]
theorem rat.preimage_cast_Iic {K : Type u_5} (a : ) :
=
@[simp]
theorem rat.preimage_cast_Ioi {K : Type u_5} (a : ) :
=
@[simp]
theorem rat.preimage_cast_Iio {K : Type u_5} (a : ) :
=
@[norm_cast]
theorem rat.cast_id (n : ) :
n = n
@[simp]
theorem rat.cast_eq_id  :
@[simp]
theorem rat.cast_hom_rat  :
@[simp]
theorem map_rat_cast {F : Type u_1} {α : Type u_3} {β : Type u_4} [ β] (f : F) (q : ) :
@[simp]
theorem eq_rat_cast {F : Type u_1} {k : Type u_2} [ k] (f : F) (r : ) :
f r = r
theorem monoid_with_zero_hom.ext_rat' {F : Type u_1} {M₀ : Type u_5} [monoid_with_zero M₀] [ 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 = 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₀] [ M₀] {f g : F} (same_on_neg_one : f (-1) = g (-1)) (same_on_pnat : ∀ (n : ), 0 < nf 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] [ 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]
def rat.subsingleton_ring_hom {R : Type u_1} [semiring R] :
@[simp, norm_cast]
theorem mul_opposite.op_rat_cast {α : Type u_3} (r : ) :
@[simp, norm_cast]
theorem mul_opposite.unop_rat_cast {α : Type u_3} (r : ) :