mathlib

6c617793 - refactor(group_theory/order_of_element): use minimal_period for the definition (#7082)

refactor(group_theory/order_of_element): use minimal_period for the definition (#7082) This PR redefines `order_of_element` in terms of `function.minimal_period`. It furthermore introduces a predicate on elements of a finite group to be of finite order. Co-authored by: Damiano Testa adomani@gmail.com Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com> Co-authored-by: adomani <adomani@gmail.com>