# Some exiled lemmas about casting #

These lemmas have been removed from `Mathlib/Data/Rat/Cast/Defs.lean` to avoiding needing to import `Mathlib/Algebra/Field/Basic.lean` there.

In fact, these lemmas don't appear to be used anywhere in Mathlib, so perhaps this file can simply be deleted.

source
@[simp]
theorem Rat.cast_pow {α : Type u_1} [DivisionRing α] (p : ℚ) (n : ℕ) :
↑(p ^ n) = ↑p ^ n
source
@[simp]
theorem Rat.cast_inv_nat {α : Type u_1} [DivisionRing α] (n : ℕ) :
↑(↑n)⁻¹ = (↑n)⁻¹
source
@[simp]
theorem Rat.cast_inv_int {α : Type u_1} [DivisionRing α] (n : ℤ) :
↑(↑n)⁻¹ = (↑n)⁻¹
source
@[simp]
theorem Rat.cast_nnratCast {K : Type u_2} [DivisionRing K] (q : ℚ≥0) :
↑↑q = ↑q
source
@[simp]
theorem Rat.cast_ofScientific {K : Type u_2} [DivisionRing K] (m : ℕ) (s : Bool) (e : ℕ) :
↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e

Casting a scientific literal via `ℚ` is the same as casting directly.

source
@[simp]
theorem NNRat.cast_pow {K : Type u_1} [DivisionSemiring K] (q : ℚ≥0) (n : ℕ) :
↑(q ^ n) = ↑q ^ n
source
theorem NNRat.cast_zpow_of_ne_zero {K : Type u_1} [DivisionSemiring K] (q : ℚ≥0) (z : ℤ) (hq : ↑q.num ≠ 0) :
↑(q ^ z) = ↑q ^ z
source
@[simp]
theorem NNRat.cast_mk {K : Type u_1} [DivisionRing K] (q : ℚ) (h : 0 ≤ q) :
↑⟨q, h⟩ = ↑q
source
theorem NNRat.Nonneg.coe_ofScientific {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (m : ℕ) (s : Bool) (e : ℕ) :
↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e