# Documentation

Mathlib.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_coe_int {α : Type u_1} [inst : ] (n : ) :
n = n
@[simp]
theorem Rat.cast_coe_nat {α : Type u_1} [inst : ] (n : ) :
n = n
@[simp]
theorem Rat.cast_zero {α : Type u_1} [inst : ] :
0 = 0
@[simp]
theorem Rat.cast_one {α : Type u_1} [inst : ] :
1 = 1
theorem Rat.cast_commute {α : Type u_1} [inst : ] (r : ) (a : α) :
Commute (r) a
theorem Rat.cast_comm {α : Type u_1} [inst : ] (r : ) (a : α) :
r * a = a * r
theorem Rat.commute_cast {α : Type u_1} [inst : ] (a : α) (r : ) :
Commute a r
theorem Rat.cast_mk_of_ne_zero {α : Type u_1} [inst : ] (a : ) (b : ) (b0 : b 0) :
↑() = a / b
theorem Rat.cast_add_of_ne_zero {α : Type u_1} [inst : ] {m : } {n : } :
m.den 0n.den 0↑(m + n) = m + n
@[simp]
theorem Rat.cast_neg {α : Type u_1} [inst : ] (n : ) :
↑(-n) = -n
theorem Rat.cast_sub_of_ne_zero {α : Type u_1} [inst : ] {m : } {n : } (m0 : m.den 0) (n0 : n.den 0) :
↑(m - n) = m - n
theorem Rat.cast_mul_of_ne_zero {α : Type u_1} [inst : ] {m : } {n : } :
m.den 0n.den 0↑(m * n) = m * n
@[simp]
theorem Rat.cast_inv_nat {α : Type u_1} [inst : ] (n : ) :
(n)⁻¹ = (n)⁻¹
@[simp]
theorem Rat.cast_inv_int {α : Type u_1} [inst : ] (n : ) :
(n)⁻¹ = (n)⁻¹
theorem Rat.cast_inv_of_ne_zero {α : Type u_1} [inst : ] {n : } :
n.num 0n.den 0n⁻¹ = (n)⁻¹
theorem Rat.cast_div_of_ne_zero {α : Type u_1} [inst : ] {m : } {n : } (md : m.den 0) (nn : n.num 0) (nd : n.den 0) :
↑(m / n) = m / n
@[simp]
theorem Rat.cast_inj {α : Type u_1} [inst : ] [inst : ] {m : } {n : } :
m = n m = n
theorem Rat.cast_injective {α : Type u_1} [inst : ] [inst : ] :
@[simp]
theorem Rat.cast_eq_zero {α : Type u_1} [inst : ] [inst : ] {n : } :
n = 0 n = 0
theorem Rat.cast_ne_zero {α : Type u_1} [inst : ] [inst : ] {n : } :
n 0 n 0
@[simp]
theorem Rat.cast_add {α : Type u_1} [inst : ] [inst : ] (m : ) (n : ) :
↑(m + n) = m + n
@[simp]
theorem Rat.cast_sub {α : Type u_1} [inst : ] [inst : ] (m : ) (n : ) :
↑(m - n) = m - n
@[simp]
theorem Rat.cast_mul {α : Type u_1} [inst : ] [inst : ] (m : ) (n : ) :
↑(m * n) = m * n
@[simp]
theorem Rat.cast_bit0 {α : Type u_1} [inst : ] [inst : ] (n : ) :
↑(bit0 n) = bit0 n
@[simp]
theorem Rat.cast_bit1 {α : Type u_1} [inst : ] [inst : ] (n : ) :
↑(bit1 n) = bit1 n
def Rat.castHom (α : Type u_1) [inst : ] [inst : ] :

Coercion ℚ → α→ α as a RingHom.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Rat.coe_cast_hom {α : Type u_1} [inst : ] [inst : ] :
↑() = Rat.cast
@[simp]
theorem Rat.cast_inv {α : Type u_1} [inst : ] [inst : ] (n : ) :
n⁻¹ = (n)⁻¹
@[simp]
theorem Rat.cast_div {α : Type u_1} [inst : ] [inst : ] (m : ) (n : ) :
↑(m / n) = m / n
@[simp]
theorem Rat.cast_zpow {α : Type u_1} [inst : ] [inst : ] (q : ) (n : ) :
↑(q ^ n) = q ^ n
theorem Rat.cast_mk {α : Type u_1} [inst : ] [inst : ] (a : ) (b : ) :
↑() = a / b
@[simp]
theorem Rat.cast_pow {α : Type u_1} [inst : ] [inst : ] (q : ) (k : ) :
↑(q ^ k) = q ^ k
theorem Rat.cast_pos_of_pos {K : Type u_1} [inst : ] {r : } (hr : 0 < r) :
0 < r
theorem Rat.cast_strictMono {K : Type u_1} [inst : ] :
StrictMono Rat.cast
theorem Rat.cast_mono {K : Type u_1} [inst : ] :
Monotone Rat.cast
@[simp]
theorem Rat.castOrderEmbedding_apply {K : Type u_1} [inst : ] :
∀ (a : ), Rat.castOrderEmbedding.toEmbedding a = a
def Rat.castOrderEmbedding {K : Type u_1} [inst : ] :

Coercion from ℚ as an order embedding.

Equations
@[simp]
theorem Rat.cast_le {K : Type u_1} [inst : ] {m : } {n : } :
m n m n
@[simp]
theorem Rat.cast_lt {K : Type u_1} [inst : ] {m : } {n : } :
m < n m < n
@[simp]
theorem Rat.cast_nonneg {K : Type u_1} [inst : ] {n : } :
0 n 0 n
@[simp]
theorem Rat.cast_nonpos {K : Type u_1} [inst : ] {n : } :
n 0 n 0
@[simp]
theorem Rat.cast_pos {K : Type u_1} [inst : ] {n : } :
0 < n 0 < n
@[simp]
theorem Rat.cast_lt_zero {K : Type u_1} [inst : ] {n : } :
n < 0 n < 0
@[simp]
theorem Rat.cast_min {K : Type u_1} [inst : ] {a : } {b : } :
↑(min a b) = min a b
@[simp]
theorem Rat.cast_max {K : Type u_1} [inst : ] {a : } {b : } :
↑(max a b) = max a b
@[simp]
theorem Rat.cast_abs {K : Type u_1} [inst : ] {q : } :
↑(abs q) = abs q
@[simp]
theorem Rat.preimage_cast_Icc {K : Type u_1} [inst : ] (a : ) (b : ) :
Rat.cast ⁻¹' Set.Icc a b = Set.Icc a b
@[simp]
theorem Rat.preimage_cast_Ico {K : Type u_1} [inst : ] (a : ) (b : ) :
Rat.cast ⁻¹' Set.Ico a b = Set.Ico a b
@[simp]
theorem Rat.preimage_cast_Ioc {K : Type u_1} [inst : ] (a : ) (b : ) :
Rat.cast ⁻¹' Set.Ioc a b = Set.Ioc a b
@[simp]
theorem Rat.preimage_cast_Ioo {K : Type u_1} [inst : ] (a : ) (b : ) :
Rat.cast ⁻¹' Set.Ioo a b = Set.Ioo a b
@[simp]
theorem Rat.preimage_cast_Ici {K : Type u_1} [inst : ] (a : ) :
Rat.cast ⁻¹' Set.Ici a =
@[simp]
theorem Rat.preimage_cast_Iic {K : Type u_1} [inst : ] (a : ) :
Rat.cast ⁻¹' Set.Iic a =
@[simp]
theorem Rat.preimage_cast_Ioi {K : Type u_1} [inst : ] (a : ) :
Rat.cast ⁻¹' Set.Ioi a =
@[simp]
theorem Rat.preimage_cast_Iio {K : Type u_1} [inst : ] (a : ) :
Rat.cast ⁻¹' Set.Iio a =
theorem Rat.cast_id (n : ) :
n = n
@[simp]
theorem Rat.cast_eq_id :
(fun x => x) = id
@[simp]
@[simp]
theorem map_ratCast {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] [inst : RingHomClass F α β] (f : F) (q : ) :
f q = q
@[simp]
theorem eq_ratCast {F : Type u_2} {k : Type u_1} [inst : ] [inst : ] (f : F) (r : ) :
f r = r
theorem MonoidWithZeroHom.ext_rat' {F : Type u_2} {M₀ : Type u_1} [inst : ] [inst : ] {f : F} {g : F} (h : ∀ (m : ), f m = g m) :
f = g

If f and g agree on the integers then they are equal φ.

theorem MonoidWithZeroHom.ext_rat {M₀ : Type u_1} [inst : ] {f : →*₀ M₀} {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 MonoidWithZeroHom.ext_rat_on_pnat {F : Type u_2} {M₀ : Type u_1} [inst : ] [inst : ] {f : 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 RingHom.ext_rat {F : Type u_2} {R : Type u_1} [inst : ] [inst : ] (f : 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_ratCast.

instance Rat.subsingleton_ringHom {R : Type u_1} [inst : ] :
Equations
@[simp]
theorem MulOpposite.op_ratCast {α : Type u_1} [inst : ] (r : ) :
{ unop := r } = r
@[simp]
theorem MulOpposite.unop_ratCast {α : Type u_1} [inst : ] (r : ) :
(r).unop = r
instance Rat.distribSMul {K : Type u_1} [inst : ] :
Equations
instance Rat.isScalarTower_right {K : Type u_1} [inst : ] :
Equations