mathlib3
e006f38c - feat(algebra/hom/iterate): Iterating an action (#13659)

Commit
3 years ago
feat(algebra/hom/iterate): Iterating an action (#13659) This PR adds `smul_iterate`, generalizing `mul_left_iterate` and `mul_right_iterate`.
Author
Parents
Loading