Commit 2021-04-21 04:20 02a31338

feat(group_theory/{order_of_element, perm/cycles}): two cycles are conjugate iff their supports have the same size (#7024) Separates out the equivs 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.