mathlib documentation

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

Tags

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

@[instance]
def rat.cast_coe {α : Type u_1} [division_ring α] :

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.

Equations
@[simp]
theorem rat.cast_of_int {α : Type u_1} [division_ring α] (n : ) :

@[simp]
theorem rat.cast_coe_int {α : Type u_1} [division_ring α] (n : ) :

@[simp]
theorem rat.cast_coe_nat {α : Type u_1} [division_ring α] (n : ) :

@[simp]
theorem rat.cast_zero {α : Type u_1} [division_ring α] :
0 = 0

@[simp]
theorem rat.cast_one {α : Type u_1} [division_ring α] :
1 = 1

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

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

theorem rat.cast_mk_of_ne_zero {α : Type u_1} [division_ring α] (a b : ) :
b 0(a /. b) = a / b

theorem rat.cast_add_of_ne_zero {α : Type u_1} [division_ring α] {m n : } :
(m.denom) 0(n.denom) 0(m + n) = m + n

@[simp]
theorem rat.cast_neg {α : Type u_1} [division_ring α] (n : ) :

theorem rat.cast_sub_of_ne_zero {α : Type u_1} [division_ring α] {m n : } :
(m.denom) 0(n.denom) 0(m - n) = m - n

theorem rat.cast_mul_of_ne_zero {α : Type u_1} [division_ring α] {m n : } :
(m.denom) 0(n.denom) 0m * n = (m) * n

theorem rat.cast_inv_of_ne_zero {α : Type u_1} [division_ring α] {n : } :
(n.num) 0(n.denom) 0n⁻¹ = (n)⁻¹

theorem rat.cast_div_of_ne_zero {α : Type u_1} [division_ring α] {m n : } :
(m.denom) 0(n.num) 0(n.denom) 0(m / n) = m / n

@[simp]
theorem rat.cast_inj {α : Type u_1} [division_ring α] [char_zero α] {m n : } :
m = n m = n

@[simp]
theorem rat.cast_eq_zero {α : Type u_1} [division_ring α] [char_zero α] {n : } :
n = 0 n = 0

theorem rat.cast_ne_zero {α : Type u_1} [division_ring α] [char_zero α] {n : } :
n 0 n 0

@[simp]
theorem rat.cast_add {α : Type u_1} [division_ring α] [char_zero α] (m n : ) :
(m + n) = m + n

@[simp]
theorem rat.cast_sub {α : Type u_1} [division_ring α] [char_zero α] (m n : ) :
(m - n) = m - n

@[simp]
theorem rat.cast_mul {α : Type u_1} [division_ring α] [char_zero α] (m n : ) :
m * n = (m) * n

@[simp]
theorem rat.cast_bit0 {α : Type u_1} [division_ring α] [char_zero α] (n : ) :

@[simp]
theorem rat.cast_bit1 {α : Type u_1} [division_ring α] [char_zero α] (n : ) :

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

Coercion ℚ → α as a ring_hom.

Equations
@[simp]
theorem rat.coe_cast_hom {α : Type u_1} [division_ring α] [char_zero α] :

@[simp]
theorem rat.cast_inv {α : Type u_1} [division_ring α] [char_zero α] (n : ) :

@[simp]
theorem rat.cast_div {α : Type u_1} [division_ring α] [char_zero α] (m n : ) :
(m / n) = m / n

theorem rat.cast_mk {α : Type u_1} [division_ring α] [char_zero α] (a b : ) :
(a /. b) = a / b

@[simp]
theorem rat.cast_pow {α : Type u_1} [division_ring α] [char_zero α] (q : ) (k : ) :
(q ^ k) = q ^ k

@[simp]
theorem rat.cast_nonneg {α : Type u_1} [linear_ordered_field α] {n : } :
0 n 0 n

@[simp]
theorem rat.cast_le {α : Type u_1} [linear_ordered_field α] {m n : } :
m n m n

@[simp]
theorem rat.cast_lt {α : Type u_1} [linear_ordered_field α] {m n : } :
m < n m < n

@[simp]
theorem rat.cast_nonpos {α : Type u_1} [linear_ordered_field α] {n : } :
n 0 n 0

@[simp]
theorem rat.cast_pos {α : Type u_1} [linear_ordered_field α] {n : } :
0 < n 0 < n

@[simp]
theorem rat.cast_lt_zero {α : Type u_1} [linear_ordered_field α] {n : } :
n < 0 n < 0

@[simp]
theorem rat.cast_id (n : ) :
n = n

@[simp]
theorem rat.cast_min {α : Type u_1} [linear_ordered_field α] {a b : } :
(min a b) = min a b

@[simp]
theorem rat.cast_max {α : Type u_1} [linear_ordered_field α] {a b : } :
(max a b) = max a b

@[simp]
theorem rat.cast_abs {α : Type u_1} [linear_ordered_field α] {q : } :

theorem ring_hom.eq_rat_cast {k : Type u_1} [division_ring k] (f : →+* k) (r : ) :
f r = r

theorem ring_hom.map_rat_cast {k : Type u_1} {k' : Type u_2} [division_ring k] [char_zero k] [division_ring k'] (f : k →+* k') (r : ) :

theorem ring_hom.ext_rat {R : Type u_1} [semiring R] (f g : →+* R) :
f = g

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