mathlib3

a83f2c26 - feat(group_theory/order_of_element): Power of subset is subgroup (#7915)

feat(group_theory/order_of_element): Power of subset is subgroup (#7915) If `S` is a nonempty subset of `G`, then `S ^ |G|` is a subgroup of `G`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>