mathlib3

ec434b75 - feat(group_theory/order_of_element): finite orderness is closed under mul (#12750)