mathlib

03e6d0ea - chore(algebra/group/hom): add `is_monoid_hom.of_mul`, use it (#1225)

chore(algebra/group/hom): add `is_monoid_hom.of_mul`, use it (#1225) * Let `to_additive` generate `is_add_monoid_hom.map_add` * Converting `is_mul_hom` into `is_monoid_hom` doesn't require `α` to be a group * Simplify the proof of `is_add_group_hom.map_sub` Avoid `simp` (without `only`)