Documentation

Mathlib.Data.Rat.Cast.CharZero

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

source
@[simp]
theorem Rat.cast_inj {α : Type u_3} [DivisionRing α] [CharZero α] {m : ℚ} {n : ℚ} :
↑m = ↑n ↔ m = n
source
theorem Rat.cast_injective {α : Type u_3} [DivisionRing α] [CharZero α] :
Function.Injective Rat.cast
source
@[simp]
theorem Rat.cast_eq_zero {α : Type u_3} [DivisionRing α] [CharZero α] {n : ℚ} :
↑n = 0 ↔ n = 0
source
theorem Rat.cast_ne_zero {α : Type u_3} [DivisionRing α] [CharZero α] {n : ℚ} :
↑n ≠ 0 ↔ n ≠ 0
source
@[simp]
theorem Rat.cast_add {α : Type u_3} [DivisionRing α] [CharZero α] (m : ℚ) (n : ℚ) :
↑(m + n) = ↑m + ↑n
source
@[simp]
theorem Rat.cast_sub {α : Type u_3} [DivisionRing α] [CharZero α] (m : ℚ) (n : ℚ) :
↑(m - n) = ↑m - ↑n
source
@[simp]
theorem Rat.cast_mul {α : Type u_3} [DivisionRing α] [CharZero α] (m : ℚ) (n : ℚ) :
↑(m * n) = ↑m * ↑n
source
@[simp]
theorem Rat.cast_bit0 {α : Type u_3} [DivisionRing α] [CharZero α] (n : ℚ) :
↑(bit0 n) = bit0 ↑n
source
@[simp]
theorem Rat.cast_bit1 {α : Type u_3} [DivisionRing α] [CharZero α] (n : ℚ) :
↑(bit1 n) = bit1 ↑n
source
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
    source
    @[simp]
    theorem Rat.coe_cast_hom {α : Type u_3} [DivisionRing α] [CharZero α] :
    ⇑(Rat.castHom α) = Rat.cast
    source
    @[simp]
    theorem Rat.cast_inv {α : Type u_3} [DivisionRing α] [CharZero α] (n : ℚ) :
    ↑n⁻¹ = (↑n)⁻¹
    source
    @[simp]
    theorem Rat.cast_div {α : Type u_3} [DivisionRing α] [CharZero α] (m : ℚ) (n : ℚ) :
    ↑(m / n) = ↑m / ↑n
    source
    @[simp]
    theorem Rat.cast_zpow {α : Type u_3} [DivisionRing α] [CharZero α] (q : ℚ) (n : ℤ) :
    ↑(q ^ n) = ↑q ^ n
    source
    theorem Rat.cast_mk {α : Type u_3} [DivisionRing α] [CharZero α] (a : ℤ) (b : ℤ) :
    ↑(Rat.divInt a b) = ↑a / ↑b
    source
    @[simp]
    theorem Rat.cast_pow {α : Type u_3} [DivisionRing α] [CharZero α] (q : ℚ) (k : ℕ) :
    ↑(q ^ k) = ↑q ^ k