Documentation

Mathlib.Data.Rat.Cast.Lemmas

Some exiled lemmas about casting #

These lemmas have been removed from Mathlib.Data.Rat.Cast.Defs to avoiding needing to import Mathlib.Algebra.Field.Basic 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
theorem NNRat.Nonneg.coe_ofScientific {K : Type u_1} [LinearOrderedField K] (m : ℕ) (s : Bool) (e : ℕ) :
↑(OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e