Commit 2019-07-14 05:25 03e6d0ea

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)