Documentation

Mathlib.Data.Rat.Cast.Defs

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.

Tags #

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

source
@[simp]
theorem NNRat.cast_natCast {α : Type u_3} [DivisionSemiring α] (n : ℕ) :
↑↑n = ↑n
source
@[simp]
theorem NNRat.cast_ofNat {α : Type u_3} [DivisionSemiring α] (n : ℕ) [n.AtLeastTwo] :
↑(OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem NNRat.cast_zero {α : Type u_3} [DivisionSemiring α] :
↑0 = 0
source
@[simp]
theorem NNRat.cast_one {α : Type u_3} [DivisionSemiring α] :
↑1 = 1
source
theorem NNRat.cast_commute {α : Type u_3} [DivisionSemiring α] (q : ℚ≥0) (a : α) :
Commute (↑q) a
source
theorem NNRat.commute_cast {α : Type u_3} [DivisionSemiring α] (a : α) (q : ℚ≥0) :
Commute a ↑q
source
theorem NNRat.cast_comm {α : Type u_3} [DivisionSemiring α] (q : ℚ≥0) (a : α) :
↑q * a = a * ↑q
source
theorem NNRat.cast_divNat_of_ne_zero {α : Type u_3} [DivisionSemiring α] (a : ℕ) {b : ℕ} (hb : ↑b ≠ 0) :
↑(divNat a b) = ↑a / ↑b
source
theorem NNRat.cast_add_of_ne_zero {α : Type u_3} [DivisionSemiring α] {q r : ℚ≥0} (hq : ↑q.den ≠ 0) (hr : ↑r.den ≠ 0) :
↑(q + r) = ↑q + ↑r
source
theorem NNRat.cast_mul_of_ne_zero {α : Type u_3} [DivisionSemiring α] {q r : ℚ≥0} (hq : ↑q.den ≠ 0) (hr : ↑r.den ≠ 0) :
↑(q * r) = ↑q * ↑r
source
theorem NNRat.cast_inv_of_ne_zero {α : Type u_3} [DivisionSemiring α] {q : ℚ≥0} (hq : ↑q.num ≠ 0) :
↑q⁻¹ = (↑q)⁻¹
source
theorem NNRat.cast_div_of_ne_zero {α : Type u_3} [DivisionSemiring α] {q r : ℚ≥0} (hq : ↑q.den ≠ 0) (hr : ↑r.num ≠ 0) :
↑(q / r) = ↑q / ↑r
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 : ℕ) [n.AtLeastTwo] :
↑(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_divInt_of_ne_zero {α : Type u_3} [DivisionRing α] (a : ℤ) {b : ℤ} (b0 : ↑b ≠ 0) :
↑(divInt a b) = ↑a / ↑b
source
theorem Rat.cast_mkRat_of_ne_zero {α : Type u_3} [DivisionRing α] (a : ℤ) {b : ℕ} (hb : ↑b ≠ 0) :
↑(mkRat a b) = ↑a / ↑b
source
theorem Rat.cast_add_of_ne_zero {α : Type u_3} [DivisionRing α] {q r : ℚ} (hq : ↑q.den ≠ 0) (hr : ↑r.den ≠ 0) :
↑(q + r) = ↑q + ↑r
source
@[simp]
theorem Rat.cast_neg {α : Type u_3} [DivisionRing α] (q : ℚ) :
↑(-q) = -↑q
source
theorem Rat.cast_sub_of_ne_zero {α : Type u_3} [DivisionRing α] {p q : ℚ} (hp : ↑p.den ≠ 0) (hq : ↑q.den ≠ 0) :
↑(p - q) = ↑p - ↑q
source
theorem Rat.cast_mul_of_ne_zero {α : Type u_3} [DivisionRing α] {p q : ℚ} (hp : ↑p.den ≠ 0) (hq : ↑q.den ≠ 0) :
↑(p * q) = ↑p * ↑q
source
theorem Rat.cast_inv_of_ne_zero {α : Type u_3} [DivisionRing α] {q : ℚ} (hq : ↑q.num ≠ 0) :
↑q⁻¹ = (↑q)⁻¹
source
theorem Rat.cast_div_of_ne_zero {α : Type u_3} [DivisionRing α] {p q : ℚ} (hp : ↑p.den ≠ 0) (hq : ↑q.num ≠ 0) :
↑(p / q) = ↑p / ↑q
source
@[simp]
theorem map_nnratCast {F : Type u_1} {α : Type u_3} {β : Type u_4} [FunLike F α β] [DivisionSemiring α] [DivisionSemiring β] [RingHomClass F α β] (f : F) (q : ℚ≥0) :
f ↑q = ↑q
source
@[simp]
theorem eq_nnratCast {F : Type u_1} {α : Type u_3} [DivisionSemiring α] [FunLike F ℚ≥0 α] [RingHomClass F ℚ≥0 α] (f : F) (q : ℚ≥0) :
f q = ↑q
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} {α : Type u_3} [DivisionRing α] [FunLike F ℚ α] [RingHomClass F ℚ α] (f : F) (q : ℚ) :
f q = ↑q
source
theorem MonoidWithZeroHomClass.ext_nnrat' {F : Type u_1} {M₀ : Type u_5} [MonoidWithZero M₀] [FunLike F ℚ≥0 M₀] [MonoidWithZeroHomClass F ℚ≥0 M₀] {f g : F} (h : ∀ (n : ℕ), f ↑n = g ↑n) :
f = g

If monoid with zero homs f and g from ℚ≥0 agree on the naturals then they are equal.

source
theorem MonoidWithZeroHomClass.ext_nnrat {M₀ : Type u_5} [MonoidWithZero M₀] {f g : ℚ≥0 →*₀ M₀} (h : f.comp ↑(Nat.castRingHom ℚ≥0) = g.comp ↑(Nat.castRingHom ℚ≥0)) :
f = g

If monoid with zero homs f and g from ℚ≥0 agree on the naturals then they are equal.

See note [partially-applied ext lemmas] for why comp is used here.

source
theorem MonoidWithZeroHomClass.ext_nnrat_iff {M₀ : Type u_5} [MonoidWithZero M₀] {f g : ℚ≥0 →*₀ M₀} :
f = g ↔ f.comp ↑(Nat.castRingHom ℚ≥0) = g.comp ↑(Nat.castRingHom ℚ≥0)
source
theorem MonoidWithZeroHomClass.ext_nnrat_on_pnat {F : Type u_1} {M₀ : Type u_5} [MonoidWithZero M₀] [FunLike F ℚ≥0 M₀] [MonoidWithZeroHomClass F ℚ≥0 M₀] {f g : F} (same_on_pnat : ∀ (n : ℕ), 0 < n → f ↑n = g ↑n) :
f = g

If monoid with zero homs f and g from ℚ≥0 agree on the positive naturals then they are equal.

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

If monoid with zero homs f and g from ℚ agree on the integers then they are equal.

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

If monoid with zero homs f and g from ℚ agree on the integers then they are equal.

See note [partially-applied ext lemmas] for why comp is used here.

source
theorem MonoidWithZeroHomClass.ext_rat_iff {M₀ : Type u_5} [MonoidWithZero M₀] {f g : ℚ →*₀ M₀} :
f = g ↔ f.comp ↑(Int.castRingHom ℚ) = g.comp ↑(Int.castRingHom ℚ)
source
theorem MonoidWithZeroHomClass.ext_rat_on_pnat {F : Type u_1} {M₀ : Type u_5} [MonoidWithZero M₀] [FunLike F ℚ M₀] [MonoidWithZeroHomClass 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

If monoid with zero homs f and g from ℚ agree on the positive naturals and -1 then they are equal.

source
theorem RingHom.ext_rat {F : Type u_1} {R : Type u_5} [Semiring R] [FunLike F ℚ R] [RingHomClass 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_ratCast.

source
instance NNRat.subsingleton_ringHom {R : Type u_5} [Semiring R] :
Subsingleton (ℚ≥0 →+* R)
source
instance Rat.subsingleton_ringHom {R : Type u_5} [Semiring R] :
Subsingleton (ℚ →+* R)