← Mathematical handbook

class Lean.Grind.LawfulOfScientific (α : Type u) [Field α] [OfScientific α] : Prop

A type class that ensures that OfScientific.ofScientific is properly defined with respect to the field structure.

• ofScientific_def {m : Nat} {s : Bool} {e : Nat} : OfScientific.ofScientific m s e = if s = true then ↑m / 10 ^ e else ↑m * 10 ^ e

  OfScientific.ofScientific is properly defined with respect to the field structure.