mathlib3

ffb99a33 - chore(algebra/group/type_tags): add `additive.to_mul` etc (#2363)

chore(algebra/group/type_tags): add `additive.to_mul` etc (#2363) Don't make `additive` and `multiplicative` irreducible (yet?) because it breaks compilation here and there. Also prove that homomorphisms from `ℕ`, `ℤ` and their `multiplicative` versions are defined by the image of `1`. Co-authored-by: Gabriel Ebner <gebner@gebner.org>