proposition: Lemma cycle_dec_conjg s a: [set (c ^ a)%g | c in cycle_dec s] = cycle_dec (s ^ a)%g.
proof: Proof. Proof using. apply esym; apply cycle_decP; constructor => [x /imsetP[x0 Hx0 ->]||]. - by apply: cyclic_conjg; apply: cyclic_dec; apply: Hx0. - by apply: disjoint_psupports_conjg; apply disjoint_cycle_dec. - have abel : abelian <<[set (c ^ a)%g | c in cycle_dec s]>>. apply abelian_disjoint_psupports; apply: disjoint_psupports_conjg. exact: disjoint_cycle_dec. rewrite [LHS](_ : _ = val (\sum_(i in [set (c ^ a)%g | c in cycle_dec s]) fmod abel i)%R); first last. rewrite -(morph_prod [morphism of fmod abel]); last by move=> i; apply: mem_gen. rewrite -[LHS](fmodK abel) //. by apply group_prod => i; apply: mem_gen. rewrite big_imset /=; last by move=> x y _ _; apply: conjg_inj. rewrite -(morph_prod [morphism of fmod abel]); first last. by move=> i Hi; apply mem_gen; apply: imset_f. rewrite fmodK; first last. by apply group_prod => i Hi; apply mem_gen; apply: imset_f. by rewrite -conjg_prod cycle_decE. 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