mathlib3

f24b01be - feat(algebra/group_power): smul and pow are monoid homs