mathlib3

02a31338 - feat(group_theory/{order_of_element, perm/cycles}): two cycles are conjugate iff their supports have the same size (#7024)

feat(group_theory/{order_of_element, perm/cycles}): two cycles are conjugate iff their supports have the same size (#7024) Separates out the `equiv`s from several proofs in `group_theory/order_of_element`. The equivs defined: `fin_equiv_powers`, `fin_equiv_gpowers`, `powers_equiv_powers`, `gpowers_equiv_gpowers`. Shows that two cyclic permutations are conjugate if and only if their supports have the same `finset.card`. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>