mathlib3

05d87671 - feat(group_theory/order_of_element): additivize (#10766)