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.

Notations #

Tags #

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

@[simp]
theorem NNRat.cast_natCast {α : Type u_3} [DivisionSemiring α] (n : ) :
n = n
@[simp]
theorem NNRat.cast_ofNat {α : Type u_3} [DivisionSemiring α] (n : ) [n.AtLeastTwo] :
@[simp]
theorem NNRat.cast_zero {α : Type u_3} [DivisionSemiring α] :
0 = 0
@[simp]
theorem NNRat.cast_one {α : Type u_3} [DivisionSemiring α] :
1 = 1
theorem NNRat.cast_commute {α : Type u_3} [DivisionSemiring α] (q : ℚ≥0) (a : α) :
Commute (↑q) a
theorem NNRat.commute_cast {α : Type u_3} [DivisionSemiring α] (a : α) (q : ℚ≥0) :
Commute a q
theorem NNRat.cast_comm {α : Type u_3} [DivisionSemiring α] (q : ℚ≥0) (a : α) :
q * a = a * q
theorem NNRat.cast_divNat_of_ne_zero {α : Type u_3} [DivisionSemiring α] (a : ) {b : } (hb : b 0) :
(NNRat.divNat a b) = a / b
theorem NNRat.cast_add_of_ne_zero {α : Type u_3} [DivisionSemiring α] {q : ℚ≥0} {r : ℚ≥0} (hq : q.den 0) (hr : r.den 0) :
(q + r) = q + r
theorem NNRat.cast_mul_of_ne_zero {α : Type u_3} [DivisionSemiring α] {q : ℚ≥0} {r : ℚ≥0} (hq : q.den 0) (hr : r.den 0) :
(q * r) = q * r
theorem NNRat.cast_inv_of_ne_zero {α : Type u_3} [DivisionSemiring α] {q : ℚ≥0} (hq : q.num 0) :
q⁻¹ = (↑q)⁻¹
theorem NNRat.cast_div_of_ne_zero {α : Type u_3} [DivisionSemiring α] {q : ℚ≥0} {r : ℚ≥0} (hq : q.den 0) (hr : r.num 0) :
(q / r) = q / r
@[simp]
theorem Rat.cast_intCast {α : Type u_3} [DivisionRing α] (n : ) :
n = n
@[simp]
theorem Rat.cast_natCast {α : Type u_3} [DivisionRing α] (n : ) :
n = n
@[deprecated Rat.cast_intCast]
theorem Rat.cast_coe_int {α : Type u_3} [DivisionRing α] (n : ) :
n = n

Alias of Rat.cast_intCast.

@[deprecated Rat.cast_natCast]
theorem Rat.cast_coe_nat {α : Type u_3} [DivisionRing α] (n : ) :
n = n

Alias of Rat.cast_natCast.

@[simp]
theorem Rat.cast_ofNat {α : Type u_3} [DivisionRing α] (n : ) [n.AtLeastTwo] :
@[simp]
theorem Rat.cast_zero {α : Type u_3} [DivisionRing α] :
0 = 0
@[simp]
theorem Rat.cast_one {α : Type u_3} [DivisionRing α] :
1 = 1
theorem Rat.cast_commute {α : Type u_3} [DivisionRing α] (r : ) (a : α) :
Commute (↑r) a
theorem Rat.cast_comm {α : Type u_3} [DivisionRing α] (r : ) (a : α) :
r * a = a * r
theorem Rat.commute_cast {α : Type u_3} [DivisionRing α] (a : α) (r : ) :
Commute a r
theorem Rat.cast_divInt_of_ne_zero {α : Type u_3} [DivisionRing α] (a : ) {b : } (b0 : b 0) :
(Rat.divInt a b) = a / b
theorem Rat.cast_mkRat_of_ne_zero {α : Type u_3} [DivisionRing α] (a : ) {b : } (hb : b 0) :
(mkRat a b) = a / b
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
@[simp]
theorem Rat.cast_neg {α : Type u_3} [DivisionRing α] (q : ) :
(-q) = -q
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
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
theorem Rat.cast_inv_of_ne_zero {α : Type u_3} [DivisionRing α] {q : } (hq : q.num 0) :
q⁻¹ = (↑q)⁻¹
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
@[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
@[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
@[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
@[simp]
theorem eq_ratCast {F : Type u_1} {α : Type u_3} [DivisionRing α] [FunLike F α] [RingHomClass F α] (f : F) (q : ) :
f q = q
theorem MonoidWithZeroHomClass.ext_nnrat' {F : Type u_1} {M₀ : Type u_5} [MonoidWithZero M₀] [FunLike F ℚ≥0 M₀] [MonoidWithZeroHomClass F ℚ≥0 M₀] {f : 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.

theorem MonoidWithZeroHomClass.ext_nnrat_iff {M₀ : Type u_5} [MonoidWithZero M₀] {f : ℚ≥0 →*₀ M₀} {g : ℚ≥0 →*₀ M₀} :
f = g f.comp (Nat.castRingHom ℚ≥0) = g.comp (Nat.castRingHom ℚ≥0)
theorem MonoidWithZeroHomClass.ext_nnrat {M₀ : Type u_5} [MonoidWithZero M₀] {f : ℚ≥0 →*₀ M₀} {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.

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 : F} {g : F} (same_on_pnat : ∀ (n : ), 0 < nf n = g n) :
f = g

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

theorem MonoidWithZeroHomClass.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 monoid with zero homs f and g from agree on the integers then they are equal.

theorem MonoidWithZeroHomClass.ext_rat_iff {M₀ : Type u_5} [MonoidWithZero M₀] {f : →*₀ M₀} {g : →*₀ M₀} :
f = g f.comp (Int.castRingHom ) = g.comp (Int.castRingHom )
theorem MonoidWithZeroHomClass.ext_rat {M₀ : Type u_5} [MonoidWithZero M₀] {f : →*₀ M₀} {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.

theorem MonoidWithZeroHomClass.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 < nf 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.

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

Equations
  • =
Equations
  • =

Scalar multiplication #

@[instance 100]
Equations
Equations
  • =
@[instance 100]
instance Rat.instDistribSMul {α : Type u_3} [DivisionRing α] :
Equations
Equations
  • =