LeanAPAP.Mathlib.Data.Rat.Cast.Lemmas

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 : ℚ≥0} {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 : ℚ≥0) (q : ℚ≥0) :

↑(p + q) = ↑p + ↑q

source

@[simp]

theorem NNRat.cast_mul {α : Type u_3} [DivisionSemiring α] [CharZero α] (p : ℚ≥0) (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_zpow {α : Type u_3} [DivisionSemiring α] [CharZero α] (q : ℚ≥0) (n : ℤ) :

↑(q ^ n) = ↑q ^ n

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 : ℚ≥0) (q : ℚ≥0) :

↑(p / q) = ↑p / ↑q

source

@[simp]

theorem NNRat.cast_divNat {α : Type u_3} [DivisionSemiring α] [CharZero α] (a : ℕ) (b : ℕ) :

↑(NNRat.divNat a b) = ↑a / ↑b