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.

source
๐Ÿ“ coverage
@[simp]
theorem Rat.cast_pow {ฮฑ : Type u_1} [DivisionRing ฮฑ] (p : โ„š) (n : โ„•) :
โ†‘(p ^ n) = โ†‘p ^ n
source
๐Ÿ“ coverage
@[simp]
theorem Rat.cast_inv_nat {ฮฑ : Type u_1} [DivisionRing ฮฑ] (n : โ„•) :
โ†‘(โ†‘n)โปยน = (โ†‘n)โปยน
source
๐Ÿ“ coverage
@[simp]
theorem Rat.cast_inv_int {ฮฑ : Type u_1} [DivisionRing ฮฑ] (n : โ„ค) :
โ†‘(โ†‘n)โปยน = (โ†‘n)โปยน
source
๐Ÿ“ coverage
@[simp]
theorem Rat.cast_nnratCast {K : Type u_2} [DivisionRing K] (q : โ„šโ‰ฅ0) :
โ†‘โ†‘q = โ†‘q
source
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[simp]
theorem NNRat.cast_pow {K : Type u_1} [DivisionSemiring K] (q : โ„šโ‰ฅ0) (n : โ„•) :
โ†‘(q ^ n) = โ†‘q ^ n
source
๐Ÿ“ coverage
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
๐Ÿ“ coverage
@[simp]
theorem NNRat.cast_mk {K : Type u_1} [DivisionRing K] (q : โ„š) (h : 0 โ‰ค q) :
โ†‘โŸจq, hโŸฉ = โ†‘q
source
๐Ÿ“ coverage
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