Commit 2021-09-24 08:36 9618d73c
View on Github →feat(algebra,group_theory): smul_(g)pow (#9311)
Rename smul_pow to smul_pow' to match smul_mul'. Instead provide the distributing lemma smul_pow where the power distributes onto the scalar as well. Provide the group action smul_gpow as well.