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.

@[simp]

theorem Rat.cast_pow {α : Type u_1} [DivisionRing α] (p : ℚ) (n : ℕ) : ↑(p ^ n) = ↑p ^ n

@[simp]

theorem Rat.cast_inv_nat {α : Type u_1} [DivisionRing α] (n : ℕ) : ↑(↑n)⁻¹ = (↑n)⁻¹

@[simp]

theorem Rat.cast_inv_int {α : Type u_1} [DivisionRing α] (n : ℤ) : ↑(↑n)⁻¹ = (↑n)⁻¹

@[simp]

theorem Rat.cast_nnratCast {K : Type u_2} [DivisionRing K] (q : ℚ≥0) : ↑↑q = ↑q

@[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.

@[simp]

theorem NNRat.cast_pow {K : Type u_1} [DivisionSemiring K] (q : ℚ≥0) (n : ℕ) : ↑(q ^ n) = ↑q ^ n

theorem NNRat.cast_zpow_of_ne_zero {K : Type u_1} [DivisionSemiring K] (q : ℚ≥0) (z : ℤ) (hq : ↑q.num ≠ 0) : ↑(q ^ z) = ↑q ^ z

@[simp]

theorem NNRat.cast_mk {K : Type u_1} [DivisionRing K] (q : ℚ) (h : 0 ≤ q) : ↑⟨q, h⟩ = ↑q

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