mathlib3

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

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.