Commit 2023-04-12 19:26 bc67aad9

View on Github →

feat: recognize scientific notation in norm_num (#1707) We implement #1706. In addition to a norm_num extension for OfScientific.ofScientific, we implement extensions for

  • Int.ofNat
  • mkRat
  • Rat.cast/RatCast.ratCast which made implementation more convenient. We also patch up the other two *.cast evaluators consistently while we're at it. We create an instance of OfScientific K for any division ring K. See Zulip discussion here for the original discussion, and this Zulip discussion for the more recent one.

Estimated changes

added theorem invOf_mul_self'
added theorem invOf_mul_self_assoc'
added theorem mul_invOf_self'
added theorem mul_invOf_self_assoc'
added theorem Rat.divInt_one
added theorem Rat.mkRat_eq_div
added theorem Rat.mkRat_one