Documentation

Mathlib.Data.Rat.Cast.CharZero

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

Stacks Tag 09FR (Characteristic zero case.)

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

Coercion ℚ → α as a RingHom.

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

      Coercion ℚ≥0 → α as a RingHom.

      Equations
        Instances For
          @[simp]
          theorem NNRat.coe_castHom {α : Type u_3} [DivisionSemiring α] [CharZero α] :
          @[simp]
          theorem NNRat.cast_inv {α : Type u_3} [DivisionSemiring α] [CharZero α] (p : ℚ≥0) :
          p⁻¹ = (↑p)⁻¹
          @[simp]
          theorem NNRat.cast_div {α : Type u_3} [DivisionSemiring α] [CharZero α] (p q : ℚ≥0) :
          ↑(p / q) = p / q
          @[simp]
          theorem NNRat.cast_zpow {α : Type u_3} [DivisionSemiring α] [CharZero α] (q : ℚ≥0) (p : ) :
          ↑(q ^ p) = q ^ p
          @[simp]
          theorem NNRat.cast_divNat {α : Type u_3} [DivisionSemiring α] [CharZero α] (a b : ) :
          (divNat a b) = a / b