feat(group_theory/order_of_element): Order in `α × β` (#18719)
The order of `(a, b)` is the lcm of the orders of `a` and `b`. Match `pow` and `zpow` lemmas. Also some `variables` noise because I could not use `x` to mean what I wanted, and incidentally the type `A` was mostly unused.
