mathlib documentation

data.rat.cast

Casts for Rational Numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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, norm_cast]

theorem rat.cast_coe_int {α : Type u_3} [division_ring α] (n : ℤ) :

@[simp, norm_cast]

theorem rat.cast_coe_nat {α : Type u_3} [division_ring α] (n : ℕ) :

@[simp, norm_cast]

theorem rat.cast_zero {α : Type u_3} [division_ring α] :

↑0 = 0

@[simp, norm_cast]

theorem rat.cast_one {α : Type u_3} [division_ring α] :

↑1 = 1

theorem rat.cast_commute {α : Type u_3} [division_ring α] (r : ℚ) (a : α) :

theorem rat.cast_comm {α : Type u_3} [division_ring α] (r : ℚ) (a : α) :

↑r * a = a * ↑r

theorem rat.commute_cast {α : Type u_3} [division_ring α] (a : α) (r : ℚ) :

@[norm_cast]

theorem rat.cast_mk_of_ne_zero {α : Type u_3} [division_ring α] (a b : ℤ) (b0 : ↑b ≠ 0) :

↑(rat.mk a b) = ↑a / ↑b

@[norm_cast]

theorem rat.cast_add_of_ne_zero {α : Type u_3} [division_ring α] {m n : ℚ} :

↑(m.denom) ≠ 0 → ↑(n.denom) ≠ 0 → ↑(m + n) = ↑m + ↑n

@[simp, norm_cast]

theorem rat.cast_neg {α : Type u_3} [division_ring α] (n : ℚ) :

@[norm_cast]

theorem rat.cast_sub_of_ne_zero {α : Type u_3} [division_ring α] {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} [division_ring α] {m n : ℚ} :

↑(m.denom) ≠ 0 → ↑(n.denom) ≠ 0 → ↑(m * n) = ↑m * ↑n

@[simp]

theorem rat.cast_inv_nat {α : Type u_3} [division_ring α] (n : ℕ) :

↑(↑n)⁻¹ = (↑n)⁻¹

@[simp]

theorem rat.cast_inv_int {α : Type u_3} [division_ring α] (n : ℤ) :

↑(↑n)⁻¹ = (↑n)⁻¹

@[norm_cast]

theorem rat.cast_inv_of_ne_zero {α : Type u_3} [division_ring α] {n : ℚ} :

↑(n.num) ≠ 0 → ↑(n.denom) ≠ 0 → ↑n⁻¹ = (↑n)⁻¹

@[norm_cast]

theorem rat.cast_div_of_ne_zero {α : Type u_3} [division_ring α] {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} [division_ring α] [char_zero α] {m n : ℚ} :

↑m = ↑n ↔ m = n

theorem rat.cast_injective {α : Type u_3} [division_ring α] [char_zero α] :

function.injective coe

@[simp]

theorem rat.cast_eq_zero {α : Type u_3} [division_ring α] [char_zero α] {n : ℚ} :

↑n = 0 ↔ n = 0

theorem rat.cast_ne_zero {α : Type u_3} [division_ring α] [char_zero α] {n : ℚ} :

↑n ≠ 0 ↔ n ≠ 0

@[simp, norm_cast]

theorem rat.cast_add {α : Type u_3} [division_ring α] [char_zero α] (m n : ℚ) :

↑(m + n) = ↑m + ↑n

@[simp, norm_cast]

theorem rat.cast_sub {α : Type u_3} [division_ring α] [char_zero α] (m n : ℚ) :

↑(m - n) = ↑m - ↑n

@[simp, norm_cast]

theorem rat.cast_mul {α : Type u_3} [division_ring α] [char_zero α] (m n : ℚ) :

↑(m * n) = ↑m * ↑n

@[simp, norm_cast]

theorem rat.cast_bit0 {α : Type u_3} [division_ring α] [char_zero α] (n : ℚ) :

↑(bit0 n) = bit0 ↑n

@[simp, norm_cast]

theorem rat.cast_bit1 {α : Type u_3} [division_ring α] [char_zero α] (n : ℚ) :

↑(bit1 n) = bit1 ↑n

def rat.cast_hom (α : Type u_3) [division_ring α] [char_zero α] :

Coercion ℚ → α as a ring_hom.

Equations

rat.cast_hom α = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

@[simp]

theorem rat.coe_cast_hom {α : Type u_3} [division_ring α] [char_zero α] :

⇑(rat.cast_hom α) = coe

@[simp, norm_cast]

theorem rat.cast_inv {α : Type u_3} [division_ring α] [char_zero α] (n : ℚ) :

↑n⁻¹ = (↑n)⁻¹

@[simp, norm_cast]

theorem rat.cast_div {α : Type u_3} [division_ring α] [char_zero α] (m n : ℚ) :

↑(m / n) = ↑m / ↑n

@[simp, norm_cast]

theorem rat.cast_zpow {α : Type u_3} [division_ring α] [char_zero α] (q : ℚ) (n : ℤ) :

↑(q ^ n) = ↑q ^ n

@[norm_cast]

theorem rat.cast_mk {α : Type u_3} [division_ring α] [char_zero α] (a b : ℤ) :

↑(rat.mk a b) = ↑a / ↑b

@[simp, norm_cast]

theorem rat.cast_pow {α : Type u_3} [division_ring α] [char_zero α] (q : ℚ) (k : ℕ) :

↑(q ^ k) = ↑q ^ k

theorem rat.cast_pos_of_pos {K : Type u_5} [linear_ordered_field K] {r : ℚ} (hr : 0 < r) :

0 < ↑r

theorem rat.cast_strict_mono {K : Type u_5} [linear_ordered_field K] :

strict_mono coe

theorem rat.cast_mono {K : Type u_5} [linear_ordered_field K] :

def rat.cast_order_embedding {K : Type u_5} [linear_ordered_field K] :

Coercion from ℚ as an order embedding.

Equations

rat.cast_order_embedding = order_embedding.of_strict_mono coe rat.cast_strict_mono

@[simp]

theorem rat.cast_order_embedding_apply {K : Type u_5} [linear_ordered_field K] (ᾰ : ℚ) :

⇑rat.cast_order_embedding ᾰ = ↑ᾰ

@[simp, norm_cast]

theorem rat.cast_le {K : Type u_5} [linear_ordered_field K] {m n : ℚ} :

↑m ≤ ↑n ↔ m ≤ n

@[simp, norm_cast]

theorem rat.cast_lt {K : Type u_5} [linear_ordered_field K] {m n : ℚ} :

↑m < ↑n ↔ m < n

@[simp]

theorem rat.cast_nonneg {K : Type u_5} [linear_ordered_field K] {n : ℚ} :

0 ≤ ↑n ↔ 0 ≤ n

@[simp]

theorem rat.cast_nonpos {K : Type u_5} [linear_ordered_field K] {n : ℚ} :

↑n ≤ 0 ↔ n ≤ 0

@[simp]

theorem rat.cast_pos {K : Type u_5} [linear_ordered_field K] {n : ℚ} :

0 < ↑n ↔ 0 < n

@[simp]

theorem rat.cast_lt_zero {K : Type u_5} [linear_ordered_field K] {n : ℚ} :

↑n < 0 ↔ n < 0

@[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, norm_cast]

theorem rat.cast_abs {K : Type u_5} [linear_ordered_field K] {q : ℚ} :

↑|q| = |↑q|

@[simp]

theorem rat.preimage_cast_Icc {K : Type u_5} [linear_ordered_field K] (a b : ℚ) :

coe ⁻¹' set.Icc ↑a ↑b = set.Icc a b

@[simp]

theorem rat.preimage_cast_Ico {K : Type u_5} [linear_ordered_field K] (a b : ℚ) :

coe ⁻¹' set.Ico ↑a ↑b = set.Ico a b

@[simp]

theorem rat.preimage_cast_Ioc {K : Type u_5} [linear_ordered_field K] (a b : ℚ) :

coe ⁻¹' set.Ioc ↑a ↑b = set.Ioc a b

@[simp]

theorem rat.preimage_cast_Ioo {K : Type u_5} [linear_ordered_field K] (a b : ℚ) :

coe ⁻¹' set.Ioo ↑a ↑b = set.Ioo a b

@[simp]

theorem rat.preimage_cast_Ici {K : Type u_5} [linear_ordered_field K] (a : ℚ) :

coe ⁻¹' set.Ici ↑a = set.Ici a

@[simp]

theorem rat.preimage_cast_Iic {K : Type u_5} [linear_ordered_field K] (a : ℚ) :

coe ⁻¹' set.Iic ↑a = set.Iic a

@[simp]

theorem rat.preimage_cast_Ioi {K : Type u_5} [linear_ordered_field K] (a : ℚ) :

coe ⁻¹' set.Ioi ↑a = set.Ioi a

@[simp]

theorem rat.preimage_cast_Iio {K : Type u_5} [linear_ordered_field K] (a : ℚ) :

coe ⁻¹' set.Iio ↑a = set.Iio a

@[norm_cast]

theorem rat.cast_id (n : ℚ) :

↑n = n

@[simp]

theorem rat.cast_eq_id :

@[simp]

theorem rat.cast_hom_rat :

rat.cast_hom ℚ = ring_hom.id ℚ

@[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 : ℚ) :

⇑f ↑q = ↑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]

def rat.subsingleton_ring_hom {R : Type u_1} [semiring R] :

subsingleton (ℚ →+* R)

@[simp, norm_cast]

theorem mul_opposite.op_rat_cast {α : Type u_3} [division_ring α] (r : ℚ) :

mul_opposite.op ↑r = ↑r

@[simp, norm_cast]

theorem mul_opposite.unop_rat_cast {α : Type u_3} [division_ring α] (r : ℚ) :

mul_opposite.unop ↑r = ↑r

@[protected, instance]

def rat.distrib_smul {K : Type u_5} [division_ring K] :

distrib_smul ℚ K

Equations

rat.distrib_smul = {to_smul_zero_class := {to_has_smul := {smul := has_smul.smul rat.smul_division_ring}, smul_zero := _}, smul_add := _}

@[protected, instance]

def rat.is_scalar_tower_right {K : Type u_5} [division_ring K] :

is_scalar_tower ℚ K K