proposition: Lemma cycle_type_conjg s a : cycle_type (s ^ a)%g = cycle_type s.
proof: Proof. Proof using. apply esym; apply val_inj => /=. rewrite porbits_conjg; apply/perm_sortP => //=. rewrite [X in perm_eq X _](eq_map (g := fun X : {set T} => #|a @: X|)); first last. by move => x; apply esym; apply card_imset; exact: perm_inj. rewrite (map_comp (fun x => #{x})); apply: perm_map. apply uniq_perm. - rewrite map_inj_uniq; first exact: enum_uniq. by apply imset_inj; apply: perm_inj. - exact: enum_uniq. - move=> x; rewrite mem_enum. apply/mapP/imsetP => [] [x0]. + by rewrite mem_enum => Hx0 ->{x}; exists x0. + by move=> Hx0 ->{x}; exists x0; rewrite ?mem_enum. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(tuple finfun finset path bigop) mathcomp(fingroup perm action) mathcomp(ssralg matrix mxalgebra algC classfun) partition tools sorted permcomp fibered_set cycles