Documentation

Mathlib.Data.Rat.Cast.OfScientific

The OfScientific instance for any characteristic zero field is well-behaved with respect to the field operations.

It's probably possible, by adjusting the OfScientific instances, to make this more general, but it's not needed at present.