mathlib

98bcabb0 - feat(group_theory/perm): add lemmas for cycles of permutations (#11955)

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. Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>