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

@[simp]

theorem Rat.cast_intCast {α : Type u_3} [DivisionRing α] (n : ℤ) :

↑↑n = ↑n

source

@[simp]

theorem Rat.cast_natCast {α : Type u_3} [DivisionRing α] (n : ℕ) :

↑↑n = ↑n

source

@[simp]

theorem Rat.cast_ofNat {α : Type u_3} [DivisionRing α] (n : ℕ) [Nat.AtLeastTwo n] :

↑(OfNat.ofNat n) = OfNat.ofNat n

source

@[simp]

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

↑0 = 0

source

@[simp]

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

↑1 = 1

source

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

Commute (↑r) a

source

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

↑r * a = a * ↑r

source

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

Commute a ↑r

source

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

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

source

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

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

source

@[simp]

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

↑(-n) = -↑n

source

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

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

source

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

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

source

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

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

source

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

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

source

theorem Rat.cast_id (n : ℚ) :

↑n = n

source

@[simp]

theorem Rat.cast_eq_id :

(fun (x : ℚ) => x) = id

source

@[simp]

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

f ↑q = ↑q

source

@[simp]

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

f r = ↑r

source

theorem MonoidWithZeroHom.ext_rat' {F : Type u_1} {M₀ : Type u_5} [MonoidWithZero M₀] [FunLike F ℚ M₀] [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

theorem MonoidWithZeroHom.ext_rat {M₀ : Type u_5} [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

theorem MonoidWithZeroHom.ext_rat_on_pnat {F : Type u_1} {M₀ : Type u_5} [MonoidWithZero M₀] [FunLike F ℚ M₀] [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