feat(algebra/group_with_zero): generalize some lemmas (#15985)
* replace `*_hom.map_inv` by a generic lemma `map_inv₀` assuming `[monoid_with_zero_hom_class]`;
* replace `*_hom.map_div` by a generic lemma `map_div₀` assuming `[monoid_with_zero_hom_class]`;
* replace `*_hom.map_zpow` by a generic lemma `map_zpow₀` assuming `[monoid_with_zero_hom_class]`;
* replace `*_hom.map_units_inv` by a generic lemma `map_units_inv` assuming `[monoid_hom_class]`, `[monoid]`, and `[division_monoid]`.
