HepLean Documentation

Mathlib.Data.Rat.Cast.CharZero

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

source
theorem Rat.cast_injective {α : Type u_3} [DivisionRing α] [CharZero α] :
Function.Injective Rat.cast

Stacks Tag 09FR (Characteristic zero case.)

source
@[simp]
theorem Rat.cast_inj {α : Type u_3} [DivisionRing α] [CharZero α] {p q : ℚ} :
↑p = ↑q ↔ p = q
source
@[simp]
theorem Rat.cast_eq_zero {α : Type u_3} [DivisionRing α] [CharZero α] {p : ℚ} :
↑p = 0 ↔ p = 0
source
theorem Rat.cast_ne_zero {α : Type u_3} [DivisionRing α] [CharZero α] {p : ℚ} :
↑p ≠ 0 ↔ p ≠ 0
source
@[simp]
theorem Rat.cast_add {α : Type u_3} [DivisionRing α] [CharZero α] (p q : ℚ) :
↑(p + q) = ↑p + ↑q
source
@[simp]
theorem Rat.cast_sub {α : Type u_3} [DivisionRing α] [CharZero α] (p q : ℚ) :
↑(p - q) = ↑p - ↑q
source
@[simp]
theorem Rat.cast_mul {α : Type u_3} [DivisionRing α] [CharZero α] (p q : ℚ) :
↑(p * q) = ↑p * ↑q
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_castHom {α : Type u_3} [DivisionRing α] [CharZero α] :
    ⇑(Rat.castHom α) = Rat.cast
    source
    @[deprecated Rat.coe_castHom]
    theorem Rat.coe_cast_hom {α : Type u_3} [DivisionRing α] [CharZero α] :
    ⇑(Rat.castHom α) = Rat.cast

    Alias of Rat.coe_castHom.

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

    Coercion ℚ≥0 → α as a RingHom.

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