norm_num plugin for scientific notation.

theorem Mathlib.Meta.NormNum.isRat_ofScientific_of_true {α : Type u_1} [DivisionRing α] {m : ℕ} {e : ℕ} {n : ℤ} {d : ℕ} : 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 α] {m : ℕ} {e : ℕ} {nm : ℕ} {ne : ℕ} {n : ℕ} : 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

def Mathlib.Meta.NormNum.evalOfScientific : Mathlib.Meta.NormNum.NormNumExt

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.