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]
@[simp]
Casting a scientific literal via ℚ
is the same as casting directly.
@[simp]
theorem
NNRat.Nonneg.coe_ofScientific
{K : Type u_1}
[Field K]
[LinearOrder K]
[IsStrictOrderedRing K]
(m : ℕ)
(s : Bool)
(e : ℕ)
: