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

source

ink

@[simp]

theorem Rat.cast_coe_int {α : Type u_1} [inst : DivisionRing α] (n : ℤ) :

↑↑n = ↑n

source

ink

@[simp]

theorem Rat.cast_coe_nat {α : Type u_1} [inst : DivisionRing α] (n : ℕ) :

↑↑n = ↑n

source

ink

@[simp]

theorem Rat.cast_zero {α : Type u_1} [inst : DivisionRing α] :

↑0 = 0

source

ink

@[simp]

theorem Rat.cast_one {α : Type u_1} [inst : DivisionRing α] :

↑1 = 1

source

ink

theorem Rat.cast_commute {α : Type u_1} [inst : DivisionRing α] (r : ℚ) (a : α) :

Commute (↑r) a

source

ink

theorem Rat.cast_comm {α : Type u_1} [inst : DivisionRing α] (r : ℚ) (a : α) :

↑r * a = a * ↑r

source

ink

theorem Rat.commute_cast {α : Type u_1} [inst : DivisionRing α] (a : α) (r : ℚ) :

Commute a ↑r

source

ink

theorem Rat.cast_mk_of_ne_zero {α : Type u_1} [inst : DivisionRing α] (a : ℤ) (b : ℤ) (b0 : ↑b ≠ 0) :

↑(Rat.divInt a b) = ↑a / ↑b

source

ink

theorem Rat.cast_add_of_ne_zero {α : Type u_1} [inst : DivisionRing α] {m : ℚ} {n : ℚ} :

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

source

ink

@[simp]

theorem Rat.cast_neg {α : Type u_1} [inst : DivisionRing α] (n : ℚ) :

↑(-n) = -↑n

source

ink

theorem Rat.cast_sub_of_ne_zero {α : Type u_1} [inst : DivisionRing α] {m : ℚ} {n : ℚ} (m0 : ↑m.den ≠ 0) (n0 : ↑n.den ≠ 0) :

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

source

ink

theorem Rat.cast_mul_of_ne_zero {α : Type u_1} [inst : DivisionRing α] {m : ℚ} {n : ℚ} :

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

source

ink

@[simp]

theorem Rat.cast_inv_nat {α : Type u_1} [inst : DivisionRing α] (n : ℕ) :

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

source

ink

@[simp]

theorem Rat.cast_inv_int {α : Type u_1} [inst : DivisionRing α] (n : ℤ) :

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

source

ink

theorem Rat.cast_inv_of_ne_zero {α : Type u_1} [inst : DivisionRing α] {n : ℚ} :

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

source

ink

theorem Rat.cast_div_of_ne_zero {α : Type u_1} [inst : DivisionRing α] {m : ℚ} {n : ℚ} (md : ↑m.den ≠ 0) (nn : ↑n.num ≠ 0) (nd : ↑n.den ≠ 0) :

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

source

ink

@[simp]

theorem Rat.cast_inj {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] {m : ℚ} {n : ℚ} :

↑m = ↑n ↔ m = n

source

ink

theorem Rat.cast_injective {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] :

Function.Injective Rat.cast

source

ink

@[simp]

theorem Rat.cast_eq_zero {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] {n : ℚ} :

↑n = 0 ↔ n = 0

source

ink

theorem Rat.cast_ne_zero {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] {n : ℚ} :

↑n ≠ 0 ↔ n ≠ 0

source

ink

@[simp]

theorem Rat.cast_add {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] (m : ℚ) (n : ℚ) :

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

source

ink

@[simp]

theorem Rat.cast_sub {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] (m : ℚ) (n : ℚ) :

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

source

ink

@[simp]

theorem Rat.cast_mul {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] (m : ℚ) (n : ℚ) :

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

source

ink

@[simp]

theorem Rat.cast_bit0 {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] (n : ℚ) :

↑(bit0 n) = bit0 ↑n

source

ink

@[simp]

theorem Rat.cast_bit1 {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] (n : ℚ) :

↑(bit1 n) = bit1 ↑n

source

ink

def Rat.castHom (α : Type u_1) [inst : DivisionRing α] [inst : CharZero α] :

ℚ →+* α

Coercion ℚ → α→ α as a RingHom.

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem Rat.coe_cast_hom {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] :

↑(Rat.castHom α) = Rat.cast

source

ink

@[simp]

theorem Rat.cast_inv {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] (n : ℚ) :

↑n⁻¹ = (↑n)⁻¹

source

ink

@[simp]

theorem Rat.cast_div {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] (m : ℚ) (n : ℚ) :

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

source

ink

@[simp]

theorem Rat.cast_zpow {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] (q : ℚ) (n : ℤ) :

↑(q ^ n) = ↑q ^ n

source

ink

theorem Rat.cast_mk {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] (a : ℤ) (b : ℤ) :

↑(Rat.divInt a b) = ↑a / ↑b

source

ink

@[simp]

theorem Rat.cast_pow {α : Type u_1} [inst : DivisionRing α] [inst : CharZero α] (q : ℚ) (k : ℕ) :

↑(q ^ k) = ↑q ^ k

source

ink

theorem Rat.cast_pos_of_pos {K : Type u_1} [inst : LinearOrderedField K] {r : ℚ} (hr : 0 < r) :

0 < ↑r

source

ink

theorem Rat.cast_strictMono {K : Type u_1} [inst : LinearOrderedField K] :

StrictMono Rat.cast

source

ink

theorem Rat.cast_mono {K : Type u_1} [inst : LinearOrderedField K] :

Monotone Rat.cast

source

ink

@[simp]

theorem Rat.castOrderEmbedding_apply {K : Type u_1} [inst : LinearOrderedField K] :

∀ (a : ℚ), ↑Rat.castOrderEmbedding.toEmbedding a = ↑a

source

ink

def Rat.castOrderEmbedding {K : Type u_1} [inst : LinearOrderedField K] :

ℚ ↪o K

Coercion from ℚ as an order embedding.

Equations

Rat.castOrderEmbedding = OrderEmbedding.ofStrictMono Rat.cast (_ : StrictMono Rat.cast)

source

ink

@[simp]

theorem Rat.cast_le {K : Type u_1} [inst : LinearOrderedField K] {m : ℚ} {n : ℚ} :

↑m ≤ ↑n ↔ m ≤ n

source

ink

@[simp]

theorem Rat.cast_lt {K : Type u_1} [inst : LinearOrderedField K] {m : ℚ} {n : ℚ} :

↑m < ↑n ↔ m < n

source

ink

@[simp]

theorem Rat.cast_nonneg {K : Type u_1} [inst : LinearOrderedField K] {n : ℚ} :

0 ≤ ↑n ↔ 0 ≤ n

source

ink

@[simp]

theorem Rat.cast_nonpos {K : Type u_1} [inst : LinearOrderedField K] {n : ℚ} :

↑n ≤ 0 ↔ n ≤ 0

source

ink

@[simp]

theorem Rat.cast_pos {K : Type u_1} [inst : LinearOrderedField K] {n : ℚ} :

0 < ↑n ↔ 0 < n

source

ink

@[simp]

theorem Rat.cast_lt_zero {K : Type u_1} [inst : LinearOrderedField K] {n : ℚ} :

↑n < 0 ↔ n < 0

source

ink

@[simp]

theorem Rat.cast_min {K : Type u_1} [inst : LinearOrderedField K] {a : ℚ} {b : ℚ} :

↑(min a b) = min ↑a ↑b

source

ink

@[simp]

theorem Rat.cast_max {K : Type u_1} [inst : LinearOrderedField K] {a : ℚ} {b : ℚ} :

↑(max a b) = max ↑a ↑b

source

ink

@[simp]

theorem Rat.cast_abs {K : Type u_1} [inst : LinearOrderedField K] {q : ℚ} :

↑(abs q) = abs ↑q

source

ink

@[simp]

theorem Rat.preimage_cast_Icc {K : Type u_1} [inst : LinearOrderedField K] (a : ℚ) (b : ℚ) :

Rat.cast ⁻¹' Set.Icc ↑a ↑b = Set.Icc a b

source

ink

@[simp]

theorem Rat.preimage_cast_Ico {K : Type u_1} [inst : LinearOrderedField K] (a : ℚ) (b : ℚ) :

Rat.cast ⁻¹' Set.Ico ↑a ↑b = Set.Ico a b

source

ink

@[simp]

theorem Rat.preimage_cast_Ioc {K : Type u_1} [inst : LinearOrderedField K] (a : ℚ) (b : ℚ) :

Rat.cast ⁻¹' Set.Ioc ↑a ↑b = Set.Ioc a b

source

ink

@[simp]

theorem Rat.preimage_cast_Ioo {K : Type u_1} [inst : LinearOrderedField K] (a : ℚ) (b : ℚ) :

Rat.cast ⁻¹' Set.Ioo ↑a ↑b = Set.Ioo a b

source

ink

@[simp]

theorem Rat.preimage_cast_Ici {K : Type u_1} [inst : LinearOrderedField K] (a : ℚ) :

Rat.cast ⁻¹' Set.Ici ↑a = Set.Ici a

source

ink

@[simp]

theorem Rat.preimage_cast_Iic {K : Type u_1} [inst : LinearOrderedField K] (a : ℚ) :

Rat.cast ⁻¹' Set.Iic ↑a = Set.Iic a

source

ink

@[simp]

theorem Rat.preimage_cast_Ioi {K : Type u_1} [inst : LinearOrderedField K] (a : ℚ) :

Rat.cast ⁻¹' Set.Ioi ↑a = Set.Ioi a

source

ink

@[simp]

theorem Rat.preimage_cast_Iio {K : Type u_1} [inst : LinearOrderedField K] (a : ℚ) :

Rat.cast ⁻¹' Set.Iio ↑a = Set.Iio a

source

ink

theorem Rat.cast_id (n : ℚ) :

↑n = n

source

ink

@[simp]

theorem Rat.cast_eq_id :

(fun x => x) = id

source

ink

@[simp]

theorem Rat.cast_hom_rat :

Rat.castHom ℚ = RingHom.id ℚ

source

ink

@[simp]

theorem map_ratCast {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : DivisionRing α] [inst : DivisionRing β] [inst : RingHomClass F α β] (f : F) (q : ℚ) :

↑f ↑q = ↑q

source

ink

@[simp]

theorem eq_ratCast {F : Type u_2} {k : Type u_1} [inst : DivisionRing k] [inst : RingHomClass F ℚ k] (f : F) (r : ℚ) :

↑f r = ↑r

source

ink

theorem MonoidWithZeroHom.ext_rat' {F : Type u_2} {M₀ : Type u_1} [inst : MonoidWithZero M₀] [inst : MonoidWithZeroHomClass F ℚ M₀] {f : F} {g : F} (h : ∀ (m : ℤ), ↑f ↑m = ↑g ↑m) :

f = g

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

source

ink

theorem MonoidWithZeroHom.ext_rat {M₀ : Type u_1} [inst : MonoidWithZero M₀] {f : ℚ →*₀ M₀} {g : ℚ →*₀ M₀} (h : MonoidWithZeroHom.comp f ↑(Int.castRingHom ℚ) = MonoidWithZeroHom.comp g ↑(Int.castRingHom ℚ)) :

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

ink

theorem MonoidWithZeroHom.ext_rat_on_pnat {F : Type u_2} {M₀ : Type u_1} [inst : MonoidWithZero M₀] [inst : MonoidWithZeroHomClass F ℚ M₀] {f : 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 φ.

source

ink