!4#1707 norm_num for scientific notation

Stream: PR reviews

[Heather Macbeth]

This PR of @Thomas Murrills has been open for two months and awaiting review on the current iteration for two weeks -- I would love to see it merged! It needs a Lean 4 meta expert to review.

[Scott Morrison]

I don't see any gotchas, although @Mario Carneiro may well! If we don't hear anything I'm happy to hit merge shortly.

[Mario Carneiro]

There is still an open question in this PR regarding the ofScientific equality argument in isRat_ofScientific_of_true, but it doesn't seem worth blocking over. I hit the merge button