mathlib

b5b26fde - feat(group_theory/order_of_element): order of a product of elements (#10399)

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. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>