mathlib3

845dcdd8 - improve naming of `to_additive`