mathlib

9c4dd02d - feat(group_theory/order_of_element): order_of_dvd_iff_gpow_eq_one (#8487)