Commit 2022-02-23 08:16 98bcabb0

feat(group_theory/perm): add lemmas for cycles of permutations (#11955) nodup_powers_of_cycle_of : shows that the the iterates of an element in the support give rise to a nodup list cycle_is_cycle_of : asserts that a given cycle c in f. cycle_factors_finset is f.cycle_of a if c a \neq a equiv.perm.sign_of_cycle_type : new formula for the sign of a permutations in terms of its cycle_type — It is simpler to use (just uses number of cycles and size of support) than the earlier lemma which is renamed as equiv.perm.sign_of_cycle_type' (it could be deleted). I made one modification to make the file compile, but I need to check compatibility with the other ones.