mathlib3

5ecb1f73 - feat(group_theory/order_of_element): order_of is the same in a submonoid (#6876)

feat(group_theory/order_of_element): order_of is the same in a submonoid (#6876) The first lemma shows that `order_of` is the same in a submonoid, but it seems like you also need a lemma for subgroups. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>