Documentation

Mathlib.Data.Rat.Cast.Lemmas

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 : ) :

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