# Casts of rational numbers into characteristic zero fields (or division rings). #

theorem Rat.cast_injective {α : Type u_3} [] [] :
@[simp]
theorem Rat.cast_inj {α : Type u_3} [] [] {p : } {q : } :
p = q p = q
@[simp]
theorem Rat.cast_eq_zero {α : Type u_3} [] [] {p : } :
p = 0 p = 0
theorem Rat.cast_ne_zero {α : Type u_3} [] [] {p : } :
p 0 p 0
@[simp]
theorem Rat.cast_add {α : Type u_3} [] [] (p : ) (q : ) :
(p + q) = p + q
@[simp]
theorem Rat.cast_sub {α : Type u_3} [] [] (p : ) (q : ) :
(p - q) = p - q
@[simp]
theorem Rat.cast_mul {α : Type u_3} [] [] (p : ) (q : ) :
(p * q) = p * q
def Rat.castHom (α : Type u_3) [] [] :

Coercion ℚ → α as a RingHom.

Equations
• = { toFun := Rat.cast, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem Rat.coe_castHom {α : Type u_3} [] [] :
(Rat.castHom α) = Rat.cast
@[deprecated Rat.coe_castHom]
theorem Rat.coe_cast_hom {α : Type u_3} [] [] :
(Rat.castHom α) = Rat.cast

Alias of Rat.coe_castHom.

@[simp]
theorem Rat.cast_inv {α : Type u_3} [] [] (p : ) :
p⁻¹ = (↑p)⁻¹
@[simp]
theorem Rat.cast_div {α : Type u_3} [] [] (p : ) (q : ) :
(p / q) = p / q
@[simp]
theorem Rat.cast_zpow {α : Type u_3} [] [] (p : ) (n : ) :
(p ^ n) = p ^ n
theorem Rat.cast_mk {α : Type u_3} [] [] (a : ) (b : ) :
(Rat.divInt a b) = a / b
theorem NNRat.cast_injective {α : Type u_3} [] [] :
@[simp]
theorem NNRat.cast_inj {α : Type u_3} [] [] {p : ℚ≥0} {q : ℚ≥0} :
p = q p = q
@[simp]
theorem NNRat.cast_eq_zero {α : Type u_3} [] [] {q : ℚ≥0} :
q = 0 q = 0
theorem NNRat.cast_ne_zero {α : Type u_3} [] [] {q : ℚ≥0} :
q 0 q 0
@[simp]
theorem NNRat.cast_add {α : Type u_3} [] [] (p : ℚ≥0) (q : ℚ≥0) :
(p + q) = p + q
@[simp]
theorem NNRat.cast_mul {α : Type u_3} [] [] (p : ℚ≥0) (q : ℚ≥0) :
(p * q) = p * q
def NNRat.castHom (α : Type u_3) [] [] :

Coercion ℚ≥0 → α as a RingHom.

Equations
• = { toFun := NNRat.cast, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem NNRat.coe_castHom {α : Type u_3} [] [] :
= NNRat.cast
@[simp]
theorem NNRat.cast_inv {α : Type u_3} [] [] (p : ℚ≥0) :
p⁻¹ = (↑p)⁻¹
@[simp]
theorem NNRat.cast_div {α : Type u_3} [] [] (p : ℚ≥0) (q : ℚ≥0) :
(p / q) = p / q
@[simp]
theorem NNRat.cast_zpow {α : Type u_3} [] [] (q : ℚ≥0) (p : ) :
(q ^ p) = q ^ p
@[simp]
theorem NNRat.cast_divNat {α : Type u_3} [] [] (a : ) (b : ) :
(NNRat.divNat a b) = a / b