mathlib

627f81b4 - feat(group_theory/order_of_element): The index-th power lands in the subgroup (#13890)

feat(group_theory/order_of_element): The index-th power lands in the subgroup (#13890) The PR adds a lemma stating `g ^ index H ∈ H`. I had to restate `G` to avoid the fintype assumption on `G`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>