def
Mathlib.Meta.NormNum.inferOfScientific
{u : Lean.Level}
(α : Q(Type u))
:
Lean.MetaM Q(OfScientific «$α»)
Helper function to synthesize a typed OfScientific α expression given DivisionRing α.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Mathlib.Meta.NormNum.isRat_ofScientific_of_true
{α : Type u_1}
[DivisionRing α]
(σα : OfScientific α)
{m : ℕ}
{e : ℕ}
{n : ℤ}
{d : ℕ}
:
(OfScientific.ofScientific = fun (m : ℕ) (s : Bool) (e : ℕ) => ↑(Rat.ofScientific m s e)) →
Mathlib.Meta.NormNum.IsRat (↑(mkRat (↑m) (10 ^ e))) n d →
Mathlib.Meta.NormNum.IsRat (OfScientific.ofScientific m true e) n d
theorem
Mathlib.Meta.NormNum.isNat_ofScientific_of_false
{α : Type u_1}
[DivisionRing α]
(σα : OfScientific α)
{m : ℕ}
{e : ℕ}
{nm : ℕ}
{ne : ℕ}
{n : ℕ}
:
(OfScientific.ofScientific = fun (m : ℕ) (s : Bool) (e : ℕ) => ↑(Rat.ofScientific m s e)) →
Mathlib.Meta.NormNum.IsNat m nm →
Mathlib.Meta.NormNum.IsNat e ne →
n = Nat.mul nm (10 ^ ne) → Mathlib.Meta.NormNum.IsNat (OfScientific.ofScientific m false e) n
The norm_num extension which identifies expressions in scientific notation, normalizing them
to rat casts if the scientific notation is inherited from the one for rationals.
Equations
- One or more equations did not get rendered due to their size.