proposition: Lemma cfConjgQuo_norm H K (phi : 'CF(H)) y : y \in 'N(K) -> y \in 'N(H) -> ((phi / K) ^ coset K y)%CF = (phi ^ y / K)%CF.
proof: Proof. move=> nKy nHy; have keryK: (K \subset cfker (phi ^ y)) = (K \subset cfker phi). by rewrite cfker_conjg // -{1}(normP nKy) conjSg. have [kerK | not_kerK] := boolP (K \subset cfker phi); last first. by rewrite !cfQuoEout ?linearZ ?rmorph1 ?cfConjg1 ?keryK. apply/cfun_inP=> _ /morphimP[x nKx Hx ->]. have nHyb: coset K y \in 'N(H / K) by rewrite inE -morphimJ ?(normP nHy). rewrite !(cfConjgE, cfQuoEnorm) ?keryK // ?in_setI ?Hx //. rewrite -morphV -?morphJ ?groupV // cfQuoEnorm //. by rewrite inE memJ_norm ?Hx ?groupJ ?groupV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop prime order) mathcomp(ssralg ssrnum finset fingroup morphism perm) mathcomp(automorphism quotient action zmodp cyclic center) mathcomp(gproduct commutator gseries nilpotent pgroup) mathcomp(sylow maximal frobenius matrix mxalgebra) mathcomp(mxrepresentation vector algC classfun character) mathcomp(archimedean)