## `norm_num` plugin for scientific notation. #

source
theorem Mathlib.Meta.NormNum.isNNRat_ofScientific_of_true {α : Type u_1} [DivisionRing α] {m e n d : ℕ} :
IsNNRat (↑(mkRat (↑m) (10 ^ e))) n d → IsNNRat (OfScientific.ofScientific m true e) n d
source
theorem Mathlib.Meta.NormNum.isNat_ofScientific_of_false {α : Type u_1} [DivisionRing α] {m e nm ne n : ℕ} :
IsNat m nm → IsNat e ne → n = nm.mul (10 ^ ne) → IsNat (OfScientific.ofScientific m false e) n
source
def Mathlib.Meta.NormNum.evalOfScientific :
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.

Instances For