Commit 2024-03-11 17:11 8939670c

Add Commute.orderOf_mul_pow_eq_lcm (#11235) We add Commute.orderOf_mul_pow_eq_lcm: if two commuting elements x and y of a monoid have order n and m, there is an element of order lcm n m. The result actually gives an explicit (computable) element, written as the product of a power of x and a power of y.