Field.toEuclideanDomain creates data

Stream: mathlib4

[Johan Commelin]

I noticed today that docs#Field.toEuclideanDomain creates data, namely the quotient and remainder functions (and the relation r) for fields. This goes against the "forgetful inheritance" doctrine. So far it doesn't seem to cause trouble in mathlib, but I wonder if we should try to fix this?

[Yaël Dillies]

I don't think it matters since fields are very boring euclidean domains

[Yaël Dillies]

As in, I don't think there's much reasoning to be done about the euclidean domain structure of a field

[Matthew Ballard]

Is that instance used anywhere?

[Johan Commelin]

No idea. But probably we should make it a def, just to be sure.

[Eric Rodriguez]

I worry that will cause more issues than the possible footguns, however :/