to_additive and extends

Stream: mathlib4

[Floris van Doorn]

Regular users of to_additive will know that it didn't manage to automatically translate instances generated by the extends clause. This is fixed in #19302.
If someone could help removing all the manual attribute declarations, that would be great! (I just did one file; to_additive will complain for all attributes that should be removed).

[Ruben Van de Velde]

Looking

[Floris van Doorn]

Thanks! That was a lot fewer errors than I expected. I guess it makes sense: for ring-like classes to_additive doesn't work anyway.

[Floris van Doorn]

The PR above is now ready for review.