mathlib
9618d73c - feat(algebra,group_theory): smul_(g)pow (#9311)

Commit
4 years ago
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. Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Author
Parents
Loading