mathlib
9078914e - feat(algebra/group): make `map_[z]pow` generic in `monoid_hom_class` (#10749)

Commit

4 years ago

feat(algebra/group): make `map_[z]pow` generic in `monoid_hom_class` (#10749) This PR makes `map_pow` take a `monoid_hom_class` instead of specifically a `monoid_hom`.

Author

Vierkantor

Parents

f46a7a0f

mathlib 9078914e - feat(algebra/group): make `map_[z]pow` generic in `monoid_hom_class` (#10749)

mathlib
9078914e - feat(algebra/group): make `map_[z]pow` generic in `monoid_hom_class` (#10749)