Commit 2022-11-25 02:14 208d8866

feat(group_theory/subgroup/basic): weaken some TC assumptions (#17698)

• Add to_additive to units.coe_to_hom_units.
• Assume that the codomain is a mul_one_class instead of a group in monoid_hom.eq_iff, monoid_hom.ker_one, monoid_hom.ker_eq_bot_iff, and monoid_hom.normal_ker.
• Add monoid_hom.ker_cod_restrict, rename monoid_hom.range_restrict_ker to monoid_hom.ker_range_restrict.
• Golf some proofs.