Documentation

Mathlib.Data.Rat.Cast.CharZero

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

@[simp]
theorem Rat.cast_inj {α : Type u_3} [DivisionRing α] [CharZero α] {m : } {n : } :
m = n m = n
@[simp]
theorem Rat.cast_eq_zero {α : Type u_3} [DivisionRing α] [CharZero α] {n : } :
n = 0 n = 0
theorem Rat.cast_ne_zero {α : Type u_3} [DivisionRing α] [CharZero α] {n : } :
n 0 n 0
@[simp]
theorem Rat.cast_add {α : Type u_3} [DivisionRing α] [CharZero α] (m : ) (n : ) :
(m + n) = m + n
@[simp]
theorem Rat.cast_sub {α : Type u_3} [DivisionRing α] [CharZero α] (m : ) (n : ) :
(m - n) = m - n
@[simp]
theorem Rat.cast_mul {α : Type u_3} [DivisionRing α] [CharZero α] (m : ) (n : ) :
(m * n) = m * n
@[simp]
theorem Rat.cast_bit0 {α : Type u_3} [DivisionRing α] [CharZero α] (n : ) :
(bit0 n) = bit0 n
@[simp]
theorem Rat.cast_bit1 {α : Type u_3} [DivisionRing α] [CharZero α] (n : ) :
(bit1 n) = bit1 n
def Rat.castHom (α : Type u_3) [DivisionRing α] [CharZero α] :

Coercion ℚ → α as a RingHom.

Equations
  • Rat.castHom α = { toFun := Rat.cast, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
    @[simp]
    theorem Rat.coe_cast_hom {α : Type u_3} [DivisionRing α] [CharZero α] :
    (Rat.castHom α) = Rat.cast
    @[simp]
    theorem Rat.cast_inv {α : Type u_3} [DivisionRing α] [CharZero α] (n : ) :
    n⁻¹ = (n)⁻¹
    @[simp]
    theorem Rat.cast_div {α : Type u_3} [DivisionRing α] [CharZero α] (m : ) (n : ) :
    (m / n) = m / n
    @[simp]
    theorem Rat.cast_zpow {α : Type u_3} [DivisionRing α] [CharZero α] (q : ) (n : ) :
    (q ^ n) = q ^ n
    theorem Rat.cast_mk {α : Type u_3} [DivisionRing α] [CharZero α] (a : ) (b : ) :
    (Rat.divInt a b) = a / b
    @[simp]
    theorem Rat.cast_pow {α : Type u_3} [DivisionRing α] [CharZero α] (q : ) (k : ) :
    (q ^ k) = q ^ k