Commit 2022-08-16 01:42 9e25db49

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].