Commit 2021-03-27 06:35 5ecb1f73
View on Github →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.