mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(algebra/group_with_zero): generalize some lemmas

Open urkud opened this issue 3 years ago • 0 comments

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

Open in Gitpod

urkud avatar Aug 10 '22 19:08 urkud