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

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

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
source
theorem rat.cast_def {α : Type u_1} [division_ring α] (r : ℚ) :
↑r = ↑(r.num) / ↑(r.denom)
source
@[simp]
theorem rat.cast_of_int {α : Type u_1} [division_ring α] (n : ℤ) :
↑(rat.of_int n) = ↑n
source
@[simp]
theorem rat.cast_coe_int {α : Type u_1} [division_ring α] (n : ℤ) :
↑↑n = ↑n
source
@[simp]
theorem rat.cast_coe_nat {α : Type u_1} [division_ring α] (n : ℕ) :
↑↑n = ↑n
source
@[simp]
theorem rat.cast_zero {α : Type u_1} [division_ring α] :
↑0 = 0
source
@[simp]
theorem rat.cast_one {α : Type u_1} [division_ring α] :
↑1 = 1
source
theorem rat.cast_commute {α : Type u_1} [division_ring α] (r : ℚ) (a : α) :
commute ↑r a
source
theorem rat.cast_comm {α : Type u_1} [division_ring α] (r : ℚ) (a : α) :
(↑r) * a = a * ↑r
source
theorem rat.commute_cast {α : Type u_1} [division_ring α] (a : α) (r : ℚ) :
commute a ↑r
source
theorem rat.cast_mk_of_ne_zero {α : Type u_1} [division_ring α] (a b : ℤ) (b0 : ↑b ≠ 0) :
↑(a /. b) = ↑a / ↑b
source
theorem rat.cast_add_of_ne_zero {α : Type u_1} [division_ring α] {m n : ℚ} :
↑(m.denom) ≠ 0 → ↑(n.denom) ≠ 0 → ↑(m + n) = ↑m + ↑n
source
@[simp]
theorem rat.cast_neg {α : Type u_1} [division_ring α] (n : ℚ) :
↑-n = -↑n
source
theorem rat.cast_sub_of_ne_zero {α : Type u_1} [division_ring α] {m n : ℚ} (m0 : ↑(m.denom) ≠ 0) (n0 : ↑(n.denom) ≠ 0) :
↑(m - n) = ↑m - ↑n
source
theorem rat.cast_mul_of_ne_zero {α : Type u_1} [division_ring α] {m n : ℚ} :
↑(m.denom) ≠ 0 → ↑(n.denom) ≠ 0 → ↑m * n = (↑m) * ↑n
source
@[simp]
theorem rat.cast_inv_nat {α : Type u_1} [division_ring α] (n : ℕ) :
↑(↑n)⁻¹ = (↑n)⁻¹
source
@[simp]
theorem rat.cast_inv_int {α : Type u_1} [division_ring α] (n : ℤ) :
↑(↑n)⁻¹ = (↑n)⁻¹
source
theorem rat.cast_inv_of_ne_zero {α : Type u_1} [division_ring α] {n : ℚ} :
↑(n.num) ≠ 0 → ↑(n.denom) ≠ 0 → ↑n⁻¹ = (↑n)⁻¹
source
theorem rat.cast_div_of_ne_zero {α : Type u_1} [division_ring α] {m n : ℚ} (md : ↑(m.denom) ≠ 0) (nn : ↑(n.num) ≠ 0) (nd : ↑(n.denom) ≠ 0) :
↑(m / n) = ↑m / ↑n
source
@[simp]
theorem rat.cast_inj {α : Type u_1} [division_ring α] [char_zero α] {m n : ℚ} :
↑m = ↑n ↔ m = n
source
theorem rat.cast_injective {α : Type u_1} [division_ring α] [char_zero α] :
function.injective coe
source
@[simp]
theorem rat.cast_eq_zero {α : Type u_1} [division_ring α] [char_zero α] {n : ℚ} :
↑n = 0 ↔ n = 0
source
theorem rat.cast_ne_zero {α : Type u_1} [division_ring α] [char_zero α] {n : ℚ} :
↑n ≠ 0 ↔ n ≠ 0
source
@[simp]
theorem rat.cast_add {α : Type u_1} [division_ring α] [char_zero α] (m n : ℚ) :
↑(m + n) = ↑m + ↑n
source
@[simp]
theorem rat.cast_sub {α : Type u_1} [division_ring α] [char_zero α] (m n : ℚ) :
↑(m - n) = ↑m - ↑n
source
@[simp]
theorem rat.cast_mul {α : Type u_1} [division_ring α] [char_zero α] (m n : ℚ) :
↑m * n = (↑m) * ↑n
source
@[simp]
theorem rat.cast_bit0 {α : Type u_1} [division_ring α] [char_zero α] (n : ℚ) :
↑(bit0 n) = bit0 ↑n
source
@[simp]
theorem rat.cast_bit1 {α : Type u_1} [division_ring α] [char_zero α] (n : ℚ) :
↑(bit1 n) = bit1 ↑n
source
def rat.cast_hom (α : Type u_1) [division_ring α] [char_zero α] :
ℚ →+* α

Coercion ℚ → α as a ring_hom.

Equations
source
@[simp]
theorem rat.coe_cast_hom {α : Type u_1} [division_ring α] [char_zero α] :
⇑(rat.cast_hom α) = coe
source
@[simp]
theorem rat.cast_inv {α : Type u_1} [division_ring α] [char_zero α] (n : ℚ) :
↑n⁻¹ = (↑n)⁻¹
source
@[simp]
theorem rat.cast_div {α : Type u_1} [division_ring α] [char_zero α] (m n : ℚ) :
↑(m / n) = ↑m / ↑n
source
theorem rat.cast_mk {α : Type u_1} [division_ring α] [char_zero α] (a b : ℤ) :
↑(a /. b) = ↑a / ↑b
source
@[simp]
theorem rat.cast_pow {α : Type u_1} [division_ring α] [char_zero α] (q : ℚ) (k : ℕ) :
↑(q ^ k) = ↑q ^ k
source
@[simp]
theorem rat.cast_nonneg {α : Type u_1} [linear_ordered_field α] {n : ℚ} :
0 ≤ ↑n ↔ 0 ≤ n
source
@[simp]
theorem rat.cast_le {α : Type u_1} [linear_ordered_field α] {m n : ℚ} :
↑m ≤ ↑n ↔ m ≤ n
source
@[simp]
theorem rat.cast_lt {α : Type u_1} [linear_ordered_field α] {m n : ℚ} :
↑m < ↑n ↔ m < n
source
@[simp]
theorem rat.cast_nonpos {α : Type u_1} [linear_ordered_field α] {n : ℚ} :
↑n ≤ 0 ↔ n ≤ 0
source
@[simp]
theorem rat.cast_pos {α : Type u_1} [linear_ordered_field α] {n : ℚ} :
0 < ↑n ↔ 0 < n
source
@[simp]
theorem rat.cast_lt_zero {α : Type u_1} [linear_ordered_field α] {n : ℚ} :
↑n < 0 ↔ n < 0
source
@[simp]
theorem rat.cast_id (n : ℚ) :
↑n = n
source
@[simp]
theorem rat.cast_min {α : Type u_1} [linear_ordered_field α] {a b : ℚ} :
↑(min a b) = min ↑a ↑b
source
@[simp]
theorem rat.cast_max {α : Type u_1} [linear_ordered_field α] {a b : ℚ} :
↑(max a b) = max ↑a ↑b
source
@[simp]
theorem rat.cast_abs {α : Type u_1} [linear_ordered_field α] {q : ℚ} :
↑|q| = |↑q|
source
theorem ring_hom.eq_rat_cast {k : Type u_1} [division_ring k] (f : ℚ →+* k) (r : ℚ) :
⇑f r = ↑r
source
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 : ℚ) :
⇑f ↑r = ↑r
source
theorem ring_hom.ext_rat {R : Type u_1} [semiring R] (f g : ℚ →+* R) :
f = g
source
@[instance]
def rat.subsingleton_ring_hom {R : Type u_1} [semiring R] :
subsingleton (ℚ →+* R)
source
@[ext]
theorem monoid_with_zero_hom.ext_rat {M : Type u_1} [group_with_zero M] {f g : monoid_with_zero_hom ℚ M} (same_on_int : f.comp (int.cast_ring_hom ℚ).to_monoid_with_zero_hom = g.comp (int.cast_ring_hom ℚ).to_monoid_with_zero_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.

source
theorem monoid_with_zero_hom.ext_rat_on_pnat {M : Type u_1} [group_with_zero M] {f g : monoid_with_zero_hom ℚ M} (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 φ.