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.
instance
instLawfulOfScientificOfCharZero
{K : Type u_1}
[Field K]
[CharZero K]
:
Lean.Grind.LawfulOfScientific K