Commit 2021-12-04 00:14 0bd9b6a3

feat(group_theory/order_of_element): order of a product of elements (#10399) The lemma is: If x and y are commuting elements of coprime orders, then the order of x * y is the product of the orders of x and y. This also gives a version for the minimal period in dynamics from which the algebraic statement is derived.