mathlib

cc14658a - chore(algebra/group_powers): Add missing lemmas (#4635)

chore(algebra/group_powers): Add missing lemmas (#4635) This part of the file defines four equivalences, but goes on to state lemmas about only one of them. This provides the lemmas for the other three.